more on complement

--- a/src/HOL/Fun.thy	Sun Jul 17 22:24:08 2011 +0200
+++ b/src/HOL/Fun.thy	Sun Jul 17 22:25:14 2011 +0200
@@ -34,15 +34,9 @@
 lemma id_apply [simp]: "id x = x"
   by (simp add: id_def)
 
-lemma image_ident [simp]: "(%x. x) ` Y = Y"
-by blast
-
 lemma image_id [simp]: "id ` Y = Y"
 by (simp add: id_def)
 
-lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
-by blast
-
 lemma vimage_id [simp]: "id -` A = A"
 by (simp add: id_def)