# HG changeset patch
# User berghofe
# Date 1210150767 -7200
# Node ID 0cb35f537c91a389912c86050fd5144f0c5f9647
# Parent  b3e8d5ec721dfc8eb7e8e7c1ffe0f842491daf96
Deleted instantiation "set :: (enum) enum"

diff -r b3e8d5ec721d -r 0cb35f537c91 src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Wed May 07 10:59:24 2008 +0200
+++ b/src/HOL/Library/Enum.thy	Wed May 07 10:59:27 2008 +0200
@@ -261,17 +261,6 @@
     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