src/HOL/Tools/Function/function.ML

     lthy'
     |> afterqed [[pattern_thm]]
   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 =
   let
     val ((goal_state, afterqed), lthy') =

     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
     |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
   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 =
   let
     val term_opt = Option.map (prep_term lthy) raw_term_opt