src/HOL/Option.thy

--- a/src/HOL/Option.thy	Tue Mar 24 15:49:32 1998 +0100
+++ b/src/HOL/Option.thy	Tue Mar 24 15:51:37 1998 +0100
@@ -18,4 +18,13 @@
   option_map	:: "('a => 'b) => ('a option => 'b option)"
  "option_map == %f y. case y of None => None | Some x => Some (f x)"
 
+consts
+
+  o2s	   :: "'a option => 'a set"
+
+primrec o2s option
+
+ "o2s  None    = {}"
+ "o2s (Some x) = {x}"
+
 end