diff -r 7a4138cb46db -r f05976d69141 src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Mon Jan 10 16:07:16 2011 +0100
+++ b/src/Pure/General/basics.ML	Mon Jan 10 16:45:28 2011 +0100
@@ -31,6 +31,7 @@
   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
@@ -90,6 +91,8 @@
 
 fun perhaps f x = the_default x (f x);
 
+fun merge_options (x, y) = if is_some x then x else y;
+
 
 (* partiality *)