diff -r 8007e4ff493a -r ea3b1b0413b4 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jan 01 11:27:29 2016 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jan 01 14:44:52 2016 +0100
@@ -208,11 +208,11 @@
   using assms by (rule effectE) (simp add: execute_simps)
 
 lemma lookup_chain:
-  "(!r \<guillemotright> f) = f"
+  "(!r \<then> f) = f"
   by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
 
 lemma update_change [code]:
-  "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
+  "r := e = change (\<lambda>_. e) r \<then> return ()"
   by (rule Heap_eqI) (simp add: change_def lookup_chain)
 
 
@@ -320,4 +320,3 @@
 code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
 
 end
-