
diff -r d1c228753d76 -r 20054fc56d17 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Feb 19 12:04:21 2014 +0100
+++ b/src/HOL/IMP/Compiler.thy	Wed Feb 19 22:02:00 2014 +1100
@@ -180,7 +180,7 @@
 "bcomp (Not b) f n = bcomp b (\<not>f) n" |
 "bcomp (And b1 b2) f n =
  (let cb2 = bcomp b2 f n;
-        m = (if f then size cb2 else (size cb2::int)+n);
+        m = if f then size cb2 else (size cb2::int)+n;
       cb1 = bcomp b1 False m
   in cb1 @ cb2)" |
 "bcomp (Less a1 a2) f n =




