# HG changeset patch
# User wenzelm
# Date 1194450181 -3600
# Node ID 63e8de11c8e9d3c57b804c5c22a82be3e8ee4a9e
# Parent  f71105742e2ca8039decce222690b60144bcbae0
attribute where/of: proper Syntax.parse/check;

diff -r f71105742e2c -r 63e8de11c8e9 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Wed Nov 07 16:43:00 2007 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Wed Nov 07 16:43:01 2007 +0100
@@ -57,6 +57,18 @@
 
 in
 
+fun read_termTs ctxt 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 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
+      |> Syntax.check_terms (ProofContext.set_mode ProofContext.mode_schematic ctxt)  (* FIXME !? *)
+      |> 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;
+
 fun read_insts ctxt mixed_insts (tvars, vars) =
   let
     val thy = ProofContext.theory_of ctxt;
@@ -105,8 +117,7 @@
 
     val (xs, strs) = split_list external_insts;
     val Ts = map (the_type vars2) xs;
-    val (ts, inferred) =   (* FIXME polymorphic!? schematic vs. 'for' context!? *)
-      ProofContext.read_termTs_schematic ctxt (K false) (K NONE) (K NONE) [] (strs ~~ Ts);
+    val (ts, inferred) = read_termTs ctxt strs Ts;
 
     val instT3 = Term.typ_subst_TVars inferred;
     val vars3 = map (apsnd instT3) vars2;