src/HOL/IOA/Solve.thy

--- a/src/HOL/IOA/Solve.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/IOA/Solve.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -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 [conjI,impI] 1 ORELSE etac conjE 1) THEN
+    REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE etac conjE 1) THEN
       asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *})
   done