diff -r f27cf421500a -r f58b7f9d3920 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Jan 07 20:18:56 2012 +0100
+++ b/src/HOL/Set.thy	Sat Jan 07 20:44:23 2012 +0100
@@ -431,10 +431,6 @@
 lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)"
   by blast
 
-lemma member_exists [code]:
-  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
-  by (rule sym) (fact bex_triv_one_point2)
-
 lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)"
   by blast
 
@@ -1837,10 +1833,6 @@
   "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
   by (simp add: project_def)
 
-lemma inter_project [code]:
-  "A \<inter> B = Set.project (\<lambda>x. x \<in> A) B"
-  by (auto simp add: project_def)
-
 instantiation set :: (equal) equal
 begin