diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/IOA/Solve.thy
--- a/src/HOL/IOA/Solve.thy	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/IOA/Solve.thy	Sat Jul 18 20:54:56 2015 +0200
@@ -145,7 +145,7 @@
   apply force
   apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
   apply (tactic {*
-    REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE etac conjE 1) THEN
+    REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE eresolve_tac @{context} [conjE] 1) THEN
       asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *})
   done