--- a/src/HOL/IMP/Compiler.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy Fri May 17 08:19:52 2013 +0200
@@ -209,7 +209,7 @@
fun ccomp :: "com \<Rightarrow> instr list" where
"ccomp SKIP = []" |
"ccomp (x ::= a) = acomp a @ [STORE x]" |
-"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
+"ccomp (c\<^isub>1;;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
(let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
in cb @ cc\<^isub>1 @ JMP (size cc\<^isub>2) # cc\<^isub>2)" |