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