# HG changeset patch
# User haftmann
# Date 1232114292 -3600
# Node ID 6fe4200532b7a4ed8a465b56db1897186137aa4d
# Parent  1ff0f3f08a7bcd53fc88a12def358fab9b66bdcd
corrected preparation of instances: parameters are proper names, not raw terms

diff -r 1ff0f3f08a7b -r 6fe4200532b7 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Jan 16 14:58:11 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Jan 16 14:58:12 2009 +0100
@@ -150,14 +150,14 @@
 
 local
 
-fun prep_inst parse_term parms (Positional insts) ctxt =
+fun prep_inst parse_term ctxt parms (Positional insts) =
       (insts ~~ parms) |> map (fn
-        (NONE, p) => Syntax.parse_term ctxt p |
+        (NONE, p) => Free (p, the (Variable.default_type ctxt p)) |
         (SOME t, _) => parse_term ctxt t)
-  | prep_inst parse_term parms (Named insts) ctxt =
+  | prep_inst parse_term ctxt parms (Named insts) =
       parms |> map (fn p => case AList.lookup (op =) insts p of
         SOME t => parse_term ctxt t |
-        NONE => Syntax.parse_term ctxt p);
+        NONE => Free (p, the (Variable.default_type ctxt p)));
 
 in
 
@@ -325,7 +325,7 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val (parm_names, parm_types) = Locale.params_of thy loc |>
-      map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
+      map_split (fn (b, SOME T, _) => (Binding.base_name b, T));
     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   in (loc, morph) end;
 
@@ -357,8 +357,9 @@
     fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
       let
         val (parm_names, parm_types) = Locale.params_of thy loc |>
-          map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
-        val inst' = parse_inst parm_names inst ctxt;
+          map_split (fn (b, SOME T, _) => (Binding.base_name b, T))
+            (*FIXME return value of Locale.params_of has strange type*)
+        val inst' = parse_inst ctxt parm_names inst;
         val parm_types' = map (TypeInfer.paramify_vars o
           Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
         val inst'' = map2 TypeInfer.constrain parm_types' inst';