1.1 --- a/src/HOL/IMP/ASM.thy	Thu Oct 27 13:52:31 2011 +0200
     1.2 +++ b/src/HOL/IMP/ASM.thy	Thu Oct 27 15:59:33 2011 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  fun comp :: "aexp \<Rightarrow> instr list" where
     1.5  "comp (N n) = [LOADI n]" |
     1.6  "comp (V x) = [LOAD x]" |
     1.7 -"comp (Plus e1 e2) = comp e1 @ comp e2 @ [ADD]"
     1.8 +"comp (Plus e\<^isub>1 e\<^isub>2) = comp e\<^isub>1 @ comp e\<^isub>2 @ [ADD]"
     1.9  text_raw{*}\end{isaverbatimwrite}*}
    1.10  
    1.11  value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"