moved misplaced comment
authornipkow
Tue Jan 11 12:58:19 1994 +0100 (1994-01-11)
changeset 224d762f9421933
parent 223 7892b76adb5b
child 225 76f60e6400e8
moved misplaced comment
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Jan 11 11:36:32 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Jan 11 12:58:19 1994 +0100
     1.3 @@ -253,7 +253,6 @@
     1.4            [] => Ctyp{sign= sign,T= T}
     1.5          | errs =>  error (cat_lines ("Error in type:" :: errs));
     1.6  
     1.7 -(*The only use is a horrible hack in the simplifier!*)
     1.8  fun read_typ(Sg{tsig,syn,...}, defS) s =
     1.9      let val term = Syntax.read syn Syntax.typeT s;
    1.10          val S0 = Type.defaultS tsig;
    1.11 @@ -295,6 +294,7 @@
    1.12        [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
    1.13      | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
    1.14  
    1.15 +(*The only use is a horrible hack in the simplifier!*)
    1.16  fun fake_cterm_of sign t =
    1.17    Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
    1.18