src/HOL/Option.thy

--- a/src/HOL/Option.thy	Tue May 30 16:08:38 2000 +0200
+++ b/src/HOL/Option.thy	Tue May 30 18:02:49 2000 +0200
@@ -10,21 +10,19 @@
 
 datatype 'a option = None | Some 'a
 
-constdefs
+consts
+  the :: "'a option => 'a"
+  o2s :: "'a option => 'a set"
 
-  the		:: "'a option => 'a"
- "the == %y. case y of None => arbitrary | Some x => x"
+primrec
+ "the (Some x) = x"
 
+primrec
+ "o2s  None    = {}"
+ "o2s (Some x) = {x}"
+
+constdefs
   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  None    = {}"
- "o2s (Some x) = {x}"
-
 end