--- a/src/HOL/IMP/Compiler.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/IMP/Compiler.thy Sat Oct 06 00:02:46 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];