diff -r d30be6791038 -r f1ae2493d93f src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Sep 12 17:39:02 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Sep 12 19:04:02 2010 +0200
@@ -879,7 +879,7 @@
     val ranT = range_type fT
 
     val default = Syntax.parse_term lthy default_str
-      |> Type_Infer.constrain fT |> Syntax.check_term lthy
+      |> Type.constraint fT |> Syntax.check_term lthy
 
     val (globals, ctxt') = fix_globals domT ranT fvar lthy