src/Pure/Isar/rule_insts.ML

 fun read_termTs ctxt schematic ss Ts =
   let
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
     val ts = map2 parse Ts ss;
     val ts' =
-      map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
+      map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
       |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
       |> Variable.polymorphic ctxt;
     val Ts' = map Term.fastype_of ts';
     val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
   in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;