--- 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}