# HG changeset patch
# User bulwahn
# Date 1350037261 -7200
# Node ID b28dbb7a45d90d3fd36c25deb05daa9e215f38b5
# Parent  77582720af965b9e5cdcd6f52bd16af078a1d82a
increading indexes to avoid clashes in the set_comprehension_pointfree simproc

diff -r 77582720af96 -r b28dbb7a45d9 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 11 23:10:49 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Oct 12 12:21:01 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