--- a/src/Pure/library.ML Wed Nov 05 11:19:15 1997 +0100
+++ b/src/Pure/library.ML Wed Nov 05 11:33:05 1997 +0100
@@ -56,10 +56,10 @@
datatype 'a option = None | Some of 'a;
-exception OPTION of string;
+exception OPTION;
fun the (Some x) = x
- | the None = raise OPTION "the";
+ | the None = raise OPTION;
fun if_none None y = y
| if_none (Some x) _ = x;
@@ -78,6 +78,12 @@
| merge_opts _ (None, some as Some _) = some
| merge_opts merge (Some x, Some y) = Some (merge (x, y));
+(*handle partial functions*)
+fun try f x = Some (f x) handle _ => None;
+fun can f x = is_some (try f x);
+
+
+
(** pairs **)
fun pair x y = (x, y);