src/ZF/Tools/datatype_package.ML

 
 fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = ProofContext.init_global thy;
     fun read_is strs =
-      map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
+      map (Syntax.parse_term ctxt #> Type.constraint @{typ i}) strs
       |> Syntax.check_terms ctxt;
 
     val rec_tms = read_is srec_tms;
     val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists;
     val dom_sum =