--- 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"