src/Pure/library.ML

   val the_default: 'a -> 'a option -> 'a
   val the_list: 'a option -> 'a list
   val if_none: 'a option -> 'a -> 'a
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
+  val perhaps: ('a -> 'a option) -> 'a -> 'a
 
   exception EXCEPTION of exn * string
   exception ERROR
   val try: ('a -> 'b) -> 'a -> 'b option
   val can: ('a -> 'b) -> 'a -> bool

   | is_some NONE = false;
 
 fun is_none (SOME _) = false
   | is_none NONE = true;
 
+fun perhaps f x =
+  case f x
+   of NONE => x
+    | SOME x' => x';
 
 (* exceptions *)
 
 exception EXCEPTION of exn * string;