src/Pure/library.ML
changeset 4046 f89dbf002604
parent 3973 1be726ef6813
child 4063 0b19014b9155
     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 **)