changeset 18333 | b356f7837921 |
parent 18330 | 444f16d232a2 |
child 18359 | 02a830bab542 |
--- a/src/Pure/library.ML Fri Dec 02 16:04:29 2005 +0100 +++ b/src/Pure/library.ML Fri Dec 02 16:04:48 2005 +0100 @@ -51,6 +51,7 @@ val if_none: 'a option -> 'a -> 'a val is_some: 'a option -> bool val is_none: 'a option -> bool + val perhaps: ('a -> 'a option) -> 'a -> 'a exception EXCEPTION of exn * string exception ERROR @@ -339,6 +340,10 @@ fun is_none (SOME _) = false | is_none NONE = true; +fun perhaps f x = + case f x + of NONE => x + | SOME x' => x'; (* exceptions *)