src/HOL/Library/Enum.thy

   with assms distinct_card [of xs]
     have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
   then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
     by (simp add: sublists_powset length_sublists)
 qed
-
-instantiation set :: (enum) enum
-begin
-
-definition
-  "enum = map set (sublists enum)"
-
-instance by default
-  (simp_all add: enum_set_def enum_all sublists_powset distinct_set_sublists enum_distinct)
-
-end
 
 instantiation nibble :: enum
 begin
 
 definition