# HG changeset patch
# User bulwahn
# Date 1350716975 -7200
# Node ID a69ec82ffae697f37a2d787a4cb24238db1cd696
# Parent  fb696ff1f0861cf2504606cbd8b90fccbdf5e1cd
improving tactic in setcomprehension_simproc

diff -r fb696ff1f086 -r a69ec82ffae6 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Oct 20 09:09:34 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Oct 20 09:09:35 2012 +0200
@@ -241,7 +241,7 @@
 
 val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
   THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
-  THEN' TRY o etac @{thm conjE}
+  THEN' REPEAT_DETERM o etac @{thm conjE}
   THEN' TRY o hyp_subst_tac;
 
 fun intro_image_tac ctxt = rtac @{thm image_eqI}