--- 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 *)