--- a/src/HOL/FixedPoint.thy Sun Nov 12 21:14:52 2006 +0100
+++ b/src/HOL/FixedPoint.thy Sun Nov 12 21:31:52 2006 +0100
@@ -112,7 +112,7 @@
done
lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
-by(simp add:SUP_def join_absorp1)
+by(simp add:SUP_def image_constant_conv join_absorp1)
subsection {* Some instances of the type class of complete lattices *}
--- a/src/HOL/Set.thy Sun Nov 12 21:14:52 2006 +0100
+++ b/src/HOL/Set.thy Sun Nov 12 21:31:52 2006 +0100
@@ -1231,7 +1231,7 @@
lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
by auto
-lemma image_constant_conv[simp]: "(%x. c) ` A = (if A = {} then {} else {c})"
+lemma image_constant_conv: "(%x. c) ` A = (if A = {} then {} else {c})"
by auto
lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"