--- a/src/HOL/Datatype.thy Sat Jan 05 09:16:11 2008 +0100
+++ b/src/HOL/Datatype.thy Sat Jan 05 09:16:27 2008 +0100
@@ -610,8 +610,13 @@
lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
by (rule set_ext, case_tac x) auto
-instance option :: (finite) finite
-proof
+instantiation option :: (finite) finite
+begin
+
+definition
+ "Finite_Set.itself = TYPE('a option)"
+
+instance proof
have "finite (UNIV :: 'a set)" by (rule finite)
hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
@@ -619,6 +624,8 @@
finally show "finite (UNIV :: 'a option set)" .
qed
+end
+
lemma univ_option [noatp, code func]:
"UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
unfolding insert_None_conv_UNIV ..