src/Pure/Isar/expression.ML
changeset 39288 f1ae2493d93f
parent 38757 2b3e054ae6fc
child 39557 fe5722fce758
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Sep 12 17:39:02 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Sep 12 19:04:02 2010 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4      (* type inference and contexts *)
     1.5      val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
     1.6      val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
     1.7 -    val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
     1.8 +    val arg = type_parms @ map2 Type.constraint parm_types' insts';
     1.9      val res = Syntax.check_terms ctxt arg;
    1.10      val ctxt' = ctxt |> fold Variable.auto_fixes res;
    1.11  
    1.12 @@ -206,7 +206,7 @@
    1.13  
    1.14  fun mk_type T = (Logic.mk_type T, []);
    1.15  fun mk_term t = (t, []);
    1.16 -fun mk_propp (p, pats) = (Syntax.type_constraint propT p, pats);
    1.17 +fun mk_propp (p, pats) = (Type.constraint propT p, pats);
    1.18  
    1.19  fun dest_type (T, []) = Logic.dest_type T;
    1.20  fun dest_term (t, []) = t;
    1.21 @@ -347,7 +347,7 @@
    1.22          val inst' = prep_inst ctxt parm_names inst;
    1.23          val parm_types' = map (Type_Infer.paramify_vars o
    1.24            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
    1.25 -        val inst'' = map2 Type_Infer.constrain parm_types' inst';
    1.26 +        val inst'' = map2 Type.constraint parm_types' inst';
    1.27          val insts' = insts @ [(loc, (prfx, inst''))];
    1.28          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
    1.29          val inst''' = insts'' |> List.last |> snd |> snd;