1.1 --- a/src/HOL/IMP/Compiler.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -201,10 +201,10 @@
     1.4  fun ccomp :: "com \<Rightarrow> instr list" where
     1.5  "ccomp SKIP = []" |
     1.6  "ccomp (x ::= a) = acomp a @ [STORE x]" |
     1.7 -"ccomp (c\<^isub>1;;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
     1.8 -"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
     1.9 -  (let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
    1.10 -   in cb @ cc\<^isub>1 @ JMP (size cc\<^isub>2) # cc\<^isub>2)" |
    1.11 +"ccomp (c\<^sub>1;;c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2" |
    1.12 +"ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
    1.13 +  (let cc\<^sub>1 = ccomp c\<^sub>1; cc\<^sub>2 = ccomp c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1)
    1.14 +   in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2)" |
    1.15  "ccomp (WHILE b DO c) =
    1.16   (let cc = ccomp c; cb = bcomp b False (size cc + 1)
    1.17    in cb @ cc @ [JMP (-(size cb + size cc + 1))])"