--- a/src/HOL/Library/Cset.thy Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Library/Cset.thy Tue Dec 21 17:52:23 2010 +0100
@@ -188,8 +188,8 @@
"map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
by (simp add: set_def)
-type_lifting map
- by (simp_all add: image_image)
+type_lifting map: map
+ by (simp_all add: fun_eq_iff image_compose)
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
[simp]: "filter P A = Set (More_Set.project P (member A))"