1.1 --- a/src/HOL/MicroJava/J/State.thy	Fri Aug 05 23:06:54 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/J/State.thy	Sun Aug 07 18:38:36 2011 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
     1.5    "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
     1.6  
     1.7 -text {* Make new_Addr completely specified (at least for the code generator) *}
     1.8 +text {* Make @{text new_Addr} completely specified (at least for the code generator) *}
     1.9  (*
    1.10  definition new_Addr  :: "aheap => loc \<times> val option" where
    1.11    "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"