diff -r ff6f60e6ab85 -r 1a0c129bb2e0 src/HOL/Hoare/HeapSyntax.thy
--- a/src/HOL/Hoare/HeapSyntax.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare/HeapSyntax.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -15,9 +15,9 @@
   "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    ("_^._" [65,1000] 65)
 translations
-  "f(r \<rightarrow> v)"  ==  "f(CONST addr r := v)"
-  "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
-  "p^.f"       =>  "f(CONST addr p)"
+  "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
+  "p^.f := e" => "f := f(p \<rightarrow> e)"
+  "p^.f" => "f(CONST addr p)"
 
 
 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]