src/HOL/IMP/ASM.thy

--- a/src/HOL/IMP/ASM.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/IMP/ASM.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -47,7 +47,7 @@
 fun comp :: "aexp \<Rightarrow> instr list" where
 "comp (N n) = [LOADI n]" |
 "comp (V x) = [LOAD x]" |
-"comp (Plus e\<^isub>1 e\<^isub>2) = comp e\<^isub>1 @ comp e\<^isub>2 @ [ADD]"
+"comp (Plus e\<^sub>1 e\<^sub>2) = comp e\<^sub>1 @ comp e\<^sub>2 @ [ADD]"
 text_raw{*}%endsnip*}
 
 value "comp (Plus (Plus (V ''x'') (N 1)) (V ''z''))"