--- a/src/Pure/thm.ML Wed Mar 15 11:25:24 1995 +0100
+++ b/src/Pure/thm.ML Wed Mar 15 12:52:03 1995 +0100
@@ -199,7 +199,7 @@
handle TYPE (msg, _, _) => error msg;
val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
val (_, t', tye) =
- Sign.infer_types sign types sorts used freeze true (ts, T');
+ Sign.infer_types sign types sorts used freeze (ts, T');
val ct = cterm_of sign t'
handle TERM (msg, _) => error msg;
in (ct, tye) end;
@@ -372,7 +372,7 @@
handle ERROR => err_in_axm name;
fun inferT_axm sg (name, pre_tm) =
- let val t = #2(Sign.infer_types sg (K None) (K None) [] true true
+ let val t = #2(Sign.infer_types sg (K None) (K None) [] true
([pre_tm], propT))
in (name, no_vars t) end
handle ERROR => err_in_axm name;