--- a/src/HOL/Bali/AxSem.thy Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Bali/AxSem.thy Sat Jul 18 20:54:56 2015 +0200
@@ -692,8 +692,9 @@
apply (erule ax_derivs.induct)
(*42 subgoals*)
apply (tactic "ALLGOALS (strip_tac @{context})")
-apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
- etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
+apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dresolve_tac @{context} @{thms subset_singletonD},
+ eresolve_tac @{context} [disjE],
+ fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
apply (tactic "TRYALL (hyp_subst_tac @{context})")
apply (simp, rule ax_derivs.empty)
apply (drule subset_insertD)