added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;

--- a/src/Pure/library.ML	Thu Oct 30 16:57:09 1997 +0100
+++ b/src/Pure/library.ML	Thu Oct 30 16:59:56 1997 +0100
@@ -73,6 +73,11 @@
 fun apsome f (Some x) = Some (f x)
   | apsome _ None = None;
 
+fun merge_opts _ (None, None) = None
+  | merge_opts _ (some as Some _, None) = some
+  | merge_opts _ (None, some as Some _) = some
+  | merge_opts merge (Some x, Some y) = Some (merge (x, y));
+
 
 
 (** pairs **)