--- a/src/Pure/drule.ML Tue Jan 04 17:05:43 2000 +0100
+++ b/src/Pure/drule.ML Wed Jan 05 11:35:18 2000 +0100
@@ -566,7 +566,7 @@
val triv_forall_equality =
let val V = read_prop "PROP V"
and QV = read_prop "!!x::'a. PROP V"
- and x = read_cterm proto_sign ("x", TFree("'a",logicS));
+ and x = read_cterm proto_sign ("x", TypeInfer.logicT);
in
store_thm "triv_forall_equality"
(equal_intr (implies_intr QV (forall_elim x (assume QV)))
--- a/src/Pure/goals.ML Tue Jan 04 17:05:43 2000 +0100
+++ b/src/Pure/goals.ML Wed Jan 05 11:35:18 2000 +0100
@@ -541,8 +541,7 @@
fun top_sg() = #sign(rep_thm(topthm()));
-fun read s = term_of (read_cterm (top_sg())
- (s, (TVar(("DUMMY",0),[]))));
+fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
(*Print a term under the current signature of the proof state*)
fun prin t = writeln (Sign.string_of_term (top_sg()) t);