--- a/src/HOL/Datatype.thy Sun Aug 24 14:24:03 2008 +0200
+++ b/src/HOL/Datatype.thy Sun Aug 24 14:42:22 2008 +0200
@@ -9,7 +9,7 @@
header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
theory Datatype
-imports Finite_Set
+imports Nat Relation
begin
typedef (Node)
@@ -605,9 +605,6 @@
lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
by (rule set_ext, case_tac x) auto
-instance option :: (finite) finite
- by default (simp add: insert_None_conv_UNIV [symmetric])
-
subsubsection {* Operations *}