# HG changeset patch
# User nipkow
# Date 1574069661 -3600
# Node ID 87fd0374b3a00dabfad2b4f8e989146d67bda688
# Parent  9de7f10675209f8f70a89a31e4013956f1f7193e
tuned

diff -r 9de7f1067520 -r 87fd0374b3a0 src/HOL/IMP/Compiler.thy
--- 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 =