# HG changeset patch
# User nipkow
# Date 758289499 -3600
# Node ID d762f9421933d9a1e0354798fe7e3910145f01f4
# Parent  7892b76adb5ba981205fdf4e130213ae5b8e09c9
moved misplaced comment

diff -r 7892b76adb5b -r d762f9421933 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Jan 11 11:36:32 1994 +0100
+++ b/src/Pure/sign.ML	Tue Jan 11 12:58:19 1994 +0100
@@ -253,7 +253,6 @@
           [] => Ctyp{sign= sign,T= T}
         | errs =>  error (cat_lines ("Error in type:" :: errs));
 
-(*The only use is a horrible hack in the simplifier!*)
 fun read_typ(Sg{tsig,syn,...}, defS) s =
     let val term = Syntax.read syn Syntax.typeT s;
         val S0 = Type.defaultS tsig;
@@ -295,6 +294,7 @@
       [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
     | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
 
+(*The only use is a horrible hack in the simplifier!*)
 fun fake_cterm_of sign t =
   Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}