src/HOL/IMP/Abs_Int1_const.thy

--- a/src/HOL/IMP/Abs_Int1_const.thy	Sun Sep 16 20:16:28 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Mon Sep 17 02:25:38 2012 +0200
@@ -74,10 +74,6 @@
 
 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)"