src/HOL/IMP/Abs_Int2_ivl.thy

--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Sun Sep 16 20:16:28 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Sep 17 02:25:38 2012 +0200
@@ -248,10 +248,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)
-
 value "show_acom_opt (AI_ivl test1_ivl)"
 
 text{* Better than @{text AI_const}: *}