added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;
authorwenzelm
Thu Oct 30 16:59:56 1997 +0100 (1997-10-30)
changeset 4046f89dbf002604
parent 4045 deda17b83bf4
child 4047 67b5552b1067
added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Oct 30 16:57:09 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Oct 30 16:59:56 1997 +0100
     1.3 @@ -73,6 +73,11 @@
     1.4  fun apsome f (Some x) = Some (f x)
     1.5    | apsome _ None = None;
     1.6  
     1.7 +fun merge_opts _ (None, None) = None
     1.8 +  | merge_opts _ (some as Some _, None) = some
     1.9 +  | merge_opts _ (None, some as Some _) = some
    1.10 +  | merge_opts merge (Some x, Some y) = Some (merge (x, y));
    1.11 +
    1.12  
    1.13  
    1.14  (** pairs **)