Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
where/of: do not allow schematic variables here!
authorwenzelm
Thu, 08 Nov 2007 20:08:11 +0100
changeset 25354 69560579abf1
parent 25353 17f04d987f37
child 25355 69c0a39ba028
where/of: do not allow schematic variables here!
src/Pure/Isar/rule_insts.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle