--- 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'