src/Pure/Isar/rule_insts.ML
changeset 37145 01aa36932739
parent 36959 f5417836dbea
child 39288 f1ae2493d93f
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4      fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
     1.5      val ts = map2 parse Ts ss;
     1.6      val ts' =
     1.7 -      map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
     1.8 +      map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
     1.9        |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
    1.10        |> Variable.polymorphic ctxt;
    1.11      val Ts' = map Term.fastype_of ts';