src/HOL/TLA/Memory/Memory.thy

--- a/src/HOL/TLA/Memory/Memory.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -189,9 +189,9 @@
       \<turnstile> Calling ch p \<and> (rs!p \<noteq> #NotAResult)
          \<longrightarrow> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
   apply (tactic
-    \<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
+    \<open>action_simp_tac \<^context> [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
   apply (tactic
-    \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm AReturn_def},
+    \<open>action_simp_tac (\<^context> addsimps [@{thm MemReturn_def}, @{thm AReturn_def},
       @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   done
 
@@ -235,12 +235,12 @@
          \<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   apply (case_tac "arg (ch w p)")
-   apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm Read_def},
-     temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1\<close>)
+   apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm Read_def},
+     temp_rewrite \<^context> @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1\<close>)
    apply (force dest: base_pair [temp_use])
   apply (erule contrapos_np)
-  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm Write_def},
-    temp_rewrite @{context} @{thm enabled_ex}])
+  apply (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm Write_def},
+    temp_rewrite \<^context> @{thm enabled_ex}])
     [@{thm WriteInner_enabled}, exI] [] 1\<close>)
   done