| changeset 4046 | f89dbf002604 |
| parent 3973 | 1be726ef6813 |
| child 4063 | 0b19014b9155 |
--- 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 **)