diff -r fd6308b4df72 -r 01aa36932739 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Thu May 27 17:41:27 2010 +0200
@@ -149,7 +149,7 @@
   end
 
 val add_function =
-  gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+  gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
 val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
 
 fun gen_function is_external prep default_constraint fixspec eqns config lthy =
@@ -163,7 +163,7 @@
   end
 
 val function =
-  gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+  gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
 val function_cmd = gen_function true Specification.read_spec "_::type"
 
 fun prepare_termination_proof prep_term raw_term_opt lthy =