# HG changeset patch
# User wenzelm
# Date 1194548891 -3600
# Node ID 69560579abf11d05cb2d3d75f359168615c84434
# Parent  17f04d987f37034efd8a91b14d79e5ac87a2f39e
where/of: do not allow schematic variables here!

diff -r 17f04d987f37 -r 69560579abf1 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Thu Nov 08 20:08:09 2007 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Thu Nov 08 20:08:11 2007 +0100
@@ -117,7 +117,7 @@
 
     val (xs, strs) = split_list external_insts;
     val Ts = map (the_type vars2) xs;
-    val (ts, inferred) = read_termTs ctxt true (* FIXME false *) strs Ts;
+    val (ts, inferred) = read_termTs ctxt false strs Ts;
 
     val instT3 = Term.typ_subst_TVars inferred;
     val vars3 = map (apsnd instT3) vars2;