diff -r 5073cb632b6c -r 73ab6d4a9236 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Oct 09 16:57:58 2012 +0200
@@ -865,10 +865,10 @@
 
 lemma project_filter:
   assumes "finite A"
-  shows "Set.project P A = filter P A"
+  shows "Set.filter P A = filter P A"
 using assms
 by (induct A) 
-  (auto simp add: filter_def project_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
+  (auto simp add: filter_def Set.filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
 
 lemma image_fold_insert:
   assumes "finite A"