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}