src/Pure/General/basics.ML

   val the: 'a option -> 'a
   val these: 'a list option -> 'a list
   val the_list: 'a option -> 'a list
   val the_default: 'a -> 'a option -> 'a
   val perhaps: ('a -> 'a option) -> 'a -> 'a
+  val merge_options: 'a option * 'a option -> 'a option
 
   (*partiality*)
   val try: ('a -> 'b) -> 'a -> 'b option
   val can: ('a -> 'b) -> 'a -> bool
 

 fun the_default x (SOME y) = y
   | the_default x NONE = x;
 
 fun perhaps f x = the_default x (f x);
 
+fun merge_options (x, y) = if is_some x then x else y;
+
 
 (* partiality *)
 
 fun try f x = SOME (f x)
   handle exn => if Exn.is_interrupt exn then reraise exn else NONE;