diff -r fd6308b4df72 -r 01aa36932739 src/HOL/Tools/hologic.ML
--- 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 *)