diff -r 0fa4389c04f9 -r a9d9f3483b71 src/HOL/IMP/Abs_State.thy
--- 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)