src/HOL/IMP/ASM.thy

--- a/src/HOL/IMP/ASM.thy	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Thu Oct 27 15:59:25 2011 +0200
@@ -48,7 +48,7 @@
 fun comp :: "aexp \<Rightarrow> instr list" where
 "comp (N n) = [LOADI n]" |
 "comp (V x) = [LOAD x]" |
-"comp (Plus e1 e2) = comp e1 @ comp e2 @ [ADD]"
+"comp (Plus e\<^isub>1 e\<^isub>2) = comp e\<^isub>1 @ comp e\<^isub>2 @ [ADD]"
 text_raw{*}\end{isaverbatimwrite}*}
 
 value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"