src/HOL/Tools/Function/function_core.ML

     val fvar = Free (fname, fT)
     val domT = domain_type fT
     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
 
     val Globals { x, h, ... } = globals