tuned

--- 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)"

--- a/src/HOL/IMP/Abs_Int1_parity.thy	Sun Sep 16 20:16:28 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Mon Sep 17 02:25:38 2012 +0200
@@ -118,10 +118,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 "test1_parity =
   ''x'' ::= N 1;
   WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"

--- 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}: *}

--- a/src/HOL/IMP/Abs_Int3.thy	Sun Sep 16 20:16:28 2012 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Mon Sep 17 02:25:38 2012 +0200
@@ -383,7 +383,7 @@
 
 subsubsection "Tests"
 
-(* FIXME dirty trick to get around some problem with the code generator *)
+(* Trick to make the code generator happy. *)
 lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y"
 by(rule refl)
 

--- a/src/HOL/IMP/Abs_State.thy	Sun Sep 16 20:16:28 2012 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Mon Sep 17 02:25:38 2012 +0200
@@ -165,6 +165,14 @@
 end
 
 
+text{* Trick to make code generator happy. *}
+lemma [code]: "L = (L :: _ \<Rightarrow> _ st set)"
+by(rule refl)
+(* L is not used in the code but is part of a type class that is used.
+   Hence the code generator wants to build a dictionary with L in it.
+   But L is not executable. This looping defn makes it look as if it were. *)
+
+
 lemma mono_fun: "F \<sqsubseteq> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
 by(auto simp: le_st_def)