diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Sat Jul 18 20:54:56 2015 +0200
@@ -1370,7 +1370,7 @@
 apply -
 apply (induct_tac "n")
 apply  (tactic "ALLGOALS (clarsimp_tac @{context})")
-apply  (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *})
+apply  (tactic {* dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1 *})
 apply    simp
 apply   (erule finite_imageI)
 apply  (simp add: MGF_asm ax_derivs_asm)