# HG changeset patch
# User wenzelm
# Date 947068518 -3600
# Node ID 78e254305ae65db805208bff6da7f8c308ddd48e
# Parent  dce06445aafdf3edbc2e2e1c62330c9845c21eb3
TypeInfer.logicT;

diff -r dce06445aafd -r 78e254305ae6 src/Pure/drule.ML
--- 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)))
diff -r dce06445aafd -r 78e254305ae6 src/Pure/goals.ML
--- 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);