tuned

--- a/src/HOL/IMP/Compiler.thy	Sun Nov 17 20:44:35 2019 +0000
+++ b/src/HOL/IMP/Compiler.thy	Mon Nov 18 10:34:21 2019 +0100
@@ -178,7 +178,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)+n;
       cb1 = bcomp b1 False m
   in cb1 @ cb2)" |
 "bcomp (Less a1 a2) f n =