diff -r f3e75541cb78 -r 935359fd8210 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Jul 18 18:52:52 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Mon Jul 18 21:15:51 2011 +0200
@@ -397,14 +397,6 @@
   shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   unfolding SUP_def less_Sup_iff by auto
 
--- "FIXME move"
-
-lemma image_ident [simp]: "(%x. x) ` Y = Y"
-  by blast
-
-lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
-  by blast
-
 class complete_boolean_algebra = boolean_algebra + complete_lattice
 begin