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.
merged
authorwenzelm
Fri, 12 Oct 2012 14:05:30 +0200
changeset 49832 2af09163cba1
parent 49831 b28dbb7a45d9 (diff)
parent 49830 28d207ba9340 (current diff)
child 49833 1d80798e8d8a
child 49837 007f03af6c6a
merged
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Oct 12 13:55:13 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Oct 12 14:05:30 2012 +0200
@@ -172,7 +172,7 @@
 fun instantiate_arg_cong ctxt pred =
   let
     val certify = cterm_of (Proof_Context.theory_of ctxt)
-    val arg_cong = @{thm arg_cong}
+    val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
     val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of arg_cong)))
   in
     cterm_instantiate [(certify f, certify pred)] arg_cong
isabelle