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