diff -r 78159411623f -r 6682c93b7d9f src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Tue Aug 09 11:00:44 2005 +0200
+++ b/src/HOL/Recdef.thy	Tue Aug 09 11:44:38 2005 +0200
@@ -79,4 +79,19 @@
   wf_same_fst
   wf_empty
 
+(* The following should really go into Datatype or Finite_Set, but
+each one lacks the other theory as a parent . . . *)
+
+lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
+by (rule set_ext, case_tac x, auto)
+
+instance option :: (finite) finite
+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"
+    by (rule insert_None_conv_UNIV)
+  finally show "finite (UNIV :: 'a option set)" .
+qed
+
 end