# HG changeset patch
# User wenzelm
# Date 878227196 -3600
# Node ID f89dbf0026047c0824056f0b414529786e2baa80
# Parent  deda17b83bf470be60cad6afc43c9c5a7f1c2ff0
added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;

diff -r deda17b83bf4 -r f89dbf002604 src/Pure/library.ML
--- 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 **)