diff -r daff3c9987cc -r 0a08c2b9b1ed src/HOL/Option.thy
--- a/src/HOL/Option.thy	Tue Nov 04 20:47:38 1997 +0100
+++ b/src/HOL/Option.thy	Tue Nov 04 20:48:38 1997 +0100
@@ -7,5 +7,15 @@
 *)
 
 Option = Arith +
+
 datatype 'a option = None | Some 'a
+
+constdefs
+
+  the		:: "'a option => 'a"
+ "the Ú %y. case y of None => arbitrary | Some x => x"
+
+  option_map	:: "('a => 'b) => ('a option => 'b option)"
+ "option_map Ú %f y. case y of None => None | Some x => Some (f x)"
+
 end