diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/IOA/Solve.thy
--- a/src/HOL/IOA/Solve.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/IOA/Solve.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -145,8 +145,8 @@
   apply force
   apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split: if_split)
   apply (tactic \<open>
-    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)\<close>)
+    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)\<close>)
   done