diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Plain.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -1,7 +1,7 @@
 header {* Plain HOL *}
 
 theory Plain
-imports Datatype FunDef Record SAT Extraction
+imports Datatype FunDef Record SAT Extraction Divides
 begin
 
 text {*
@@ -9,6 +9,9 @@
   include @{text Hilbert_Choice}.
 *}
 
+instance option :: (finite) finite
+  by default (simp add: insert_None_conv_UNIV [symmetric])
+
 ML {* path_add "~~/src/HOL/Library" *}
 
 end