src/HOL/hologic.ML

--- a/src/HOL/hologic.ML	Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/hologic.ML	Wed Jan 05 11:56:04 2000 +0100
@@ -9,7 +9,7 @@
 sig
   val termC: class
   val termS: sort
-  val termTVar: typ
+  val termT: typ
   val boolT: typ
   val false_const: term
   val true_const: term
@@ -75,8 +75,7 @@
 
 val termC: class = "term";
 val termS: sort = [termC];
-
-val termTVar = TVar (("'a", 0), termS);
+val termT = TypeInfer.anyT termS;
 
 
 (* bool and set *)