1.1 --- a/src/HOL/IMP/Compiler.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -39,9 +39,9 @@
     1.4  "compile (x:==a) = [ASIN x a]"
     1.5  "compile (c1;c2) = compile c1 @ compile c2"
     1.6  "compile (IF b THEN c1 ELSE c2) =
     1.7 - [JMPF b (length(compile c1)+2)] @ compile c1 @
     1.8 + [JMPF b (length(compile c1) + # 2)] @ compile c1 @
     1.9   [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
    1.10 -"compile (WHILE b DO c) = [JMPF b (length(compile c)+2)] @ compile c @
    1.11 +"compile (WHILE b DO c) = [JMPF b (length(compile c) + # 2)] @ compile c @
    1.12   [JMPB (length(compile c)+1)]"
    1.13  
    1.14  declare nth_append[simp];