diff -r 323414474c1f -r 73fb17ed2e08 src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Sun Sep 16 10:33:25 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Sun Sep 16 11:50:03 2012 +0200
@@ -20,7 +20,7 @@
   (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
 by(auto split: prod.split const.split)
 
-instantiation const :: SL_top
+instantiation const :: semilattice
 begin
 
 fun le_const where
@@ -74,6 +74,10 @@
 
 subsubsection "Tests"
 
+(* FIXME dirty trick to get around some problem with the code generator *)
+lemma [code]: "L X = (L X :: 'av::semilattice st set)"
+by(rule refl)
+
 definition "steps c i = (step_const(top c) ^^ i) (bot c)"
 
 value "show_acom (steps test1_const 0)"