diff -r 967728367ad9 -r 50673b362324 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Sep 27 17:20:02 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Fri Sep 27 17:57:30 2013 +0200
@@ -32,6 +32,14 @@
   (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
 by (induction xs arbitrary: i) (auto simp: algebra_simps)
 
+text{* We hide coercion @{const int} applied to @{const length}: *}
+
+abbreviation (output)
+  "isize xs == int (length xs)"
+
+notation isize ("size")
+
+
 subsection "Instructions and Stack Machine"
 
 text_raw{*\snip{instrdef}{0}{1}{% *}