# HG changeset patch
# User wenzelm
# Date 878725985 -3600
# Node ID e1659fd7a221bc014c277bced01a350f636bc641
# Parent  af6743b065fbe70183572ab462e9a3f672c2e47d
fixed exception OPTION;
added try, can;

diff -r af6743b065fb -r e1659fd7a221 src/Pure/library.ML
--- 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);