diff -r 5b946c81dfbf -r 324bc1ffba12 src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 21:21:02 2016 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Mon Jan 11 22:23:03 2016 +0100
@@ -178,7 +178,7 @@
 *)
 
 lemma Memoryidle: "\<turnstile> \<not>$(Calling ch p) \<longrightarrow> \<not> RNext ch mm rs p"
-  by (auto simp: Return_def RM_action_defs)
+  by (auto simp: AReturn_def RM_action_defs)
 
 (* Enabledness conditions *)
 
@@ -191,7 +191,7 @@
   apply (tactic
     \<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 Return_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