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