src/ZF/Tools/inductive_package.ML

 (*source version*)
 fun add_inductive (srec_tms, sdom_sum) intr_srcs
     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = ProofContext.init_global thy;
-    val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
+    val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
       #> Syntax.check_terms ctxt;
 
     val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
     val sintrs = map fst intr_srcs ~~ intr_atts;
     val rec_tms = read_terms srec_tms;