diff -r 5073cb632b6c -r 73ab6d4a9236 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/HOL/Set.thy	Tue Oct 09 16:57:58 2012 +0200
@@ -1825,14 +1825,14 @@
   "x \<in> Set.remove y A \<longleftrightarrow> x \<in> A \<and> x \<noteq> y"
   by (simp add: remove_def)
 
-definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  [code_abbrev]: "project P A = {a \<in> A. P a}"
-
-hide_const (open) project
-
-lemma member_project [simp]:
-  "x \<in> Set.project P A \<longleftrightarrow> x \<in> A \<and> P x"
-  by (simp add: project_def)
+definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  [code_abbrev]: "filter P A = {a \<in> A. P a}"
+
+hide_const (open) filter
+
+lemma member_filter [simp]:
+  "x \<in> Set.filter P A \<longleftrightarrow> x \<in> A \<and> P x"
+  by (simp add: filter_def)
 
 instantiation set :: (equal) equal
 begin