instantiation option :: (enum) enum

--- a/src/HOL/Library/Enum.thy	Tue Dec 09 11:49:12 2008 -0800
+++ b/src/HOL/Library/Enum.thy	Tue Dec 09 12:53:25 2008 -0800
@@ -365,4 +365,15 @@
 
 end
 
-end
\ No newline at end of file
+instantiation option :: (enum) enum
+begin
+
+definition
+  "enum = None # map Some enum"
+
+instance by default
+  (auto simp add: enum_all enum_option_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
+
+end
+
+end