src/HOL/Tools/hologic.ML
changeset 37145 01aa36932739
parent 36692 54b64d4ad524
child 37387 3581483cca6c
--- a/src/HOL/Tools/hologic.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu May 27 17:41:27 2010 +0200
@@ -138,7 +138,7 @@
 (* HOL syntax *)
 
 val typeS: sort = ["HOL.type"];
-val typeT = TypeInfer.anyT typeS;
+val typeT = Type_Infer.anyT typeS;
 
 
 (* bool and set *)