1.1 --- a/src/Pure/Isar/expression.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -162,9 +162,9 @@
     1.4      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
     1.5  
     1.6      (* type inference and contexts *)
     1.7 -    val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types;
     1.8 +    val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
     1.9      val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
    1.10 -    val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
    1.11 +    val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
    1.12      val res = Syntax.check_terms ctxt arg;
    1.13      val ctxt' = ctxt |> fold Variable.auto_fixes res;
    1.14  
    1.15 @@ -345,9 +345,9 @@
    1.16        let
    1.17          val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
    1.18          val inst' = prep_inst ctxt parm_names inst;
    1.19 -        val parm_types' = map (TypeInfer.paramify_vars o
    1.20 +        val parm_types' = map (Type_Infer.paramify_vars o
    1.21            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
    1.22 -        val inst'' = map2 TypeInfer.constrain parm_types' inst';
    1.23 +        val inst'' = map2 Type_Infer.constrain parm_types' inst';
    1.24          val insts' = insts @ [(loc, (prfx, inst''))];
    1.25          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
    1.26          val inst''' = insts'' |> List.last |> snd |> snd;