diff -r a01b2de0e3e1 -r 4d1185c77f4a src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri Mar 06 20:30:16 2009 +0100
+++ b/src/HOL/Option.thy	Fri Mar 06 20:30:17 2009 +0100
@@ -5,7 +5,7 @@
 header {* Datatype option *}
 
 theory Option
-imports Datatype
+imports Datatype Finite_Set
 begin
 
 datatype 'a option = None | Some 'a
@@ -30,6 +30,9 @@
 lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
   by (rule set_ext, case_tac x) auto
 
+instance option :: (finite) finite proof
+qed (simp add: insert_None_conv_UNIV [symmetric])
+
 lemma inj_Some [simp]: "inj_on Some A"
   by (rule inj_onI) simp