diff -r a0e6bda62b7b -r 3d51fbf81c17 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/IMP/Compiler.thy	Fri Oct 05 21:52:39 2001 +0200
@@ -39,9 +39,9 @@
 "compile (x:==a) = [ASIN x a]"
 "compile (c1;c2) = compile c1 @ compile c2"
 "compile (IF b THEN c1 ELSE c2) =
- [JMPF b (length(compile c1)+2)] @ compile c1 @
+ [JMPF b (length(compile c1) + # 2)] @ compile c1 @
  [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
-"compile (WHILE b DO c) = [JMPF b (length(compile c)+2)] @ compile c @
+"compile (WHILE b DO c) = [JMPF b (length(compile c) + # 2)] @ compile c @
  [JMPB (length(compile c)+1)]"
 
 declare nth_append[simp];