diff -r 5288fa24c9db -r c0186a0d8cb3 src/HOL/BNF/Tools/bnf_comp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Mon Oct 21 23:45:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Tue Oct 22 14:17:12 2013 +0200
@@ -164,10 +164,9 @@
 fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms =
   ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
   unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN
-  REPEAT_DETERM (
-    atac 1 ORELSE
-    REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
-    (TRY o dresolve_tac Gwit_thms THEN'
+  REPEAT_DETERM ((atac ORELSE'
+    REPEAT_DETERM o eresolve_tac @{thms UnionE UnE} THEN'
+    etac imageE THEN' TRY o dresolve_tac Gwit_thms THEN'
     (etac FalseE ORELSE'
     hyp_subst_tac ctxt THEN'
     dresolve_tac Fwit_thms THEN'