src/Pure/library.ML
changeset 4139 e1659fd7a221
parent 4102 f746af27164b
child 4181 fcc8b47e4c49
     1.1 --- a/src/Pure/library.ML	Wed Nov 05 11:19:15 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Nov 05 11:33:05 1997 +0100
     1.3 @@ -56,10 +56,10 @@
     1.4  
     1.5  datatype 'a option = None | Some of 'a;
     1.6  
     1.7 -exception OPTION of string;
     1.8 +exception OPTION;
     1.9  
    1.10  fun the (Some x) = x
    1.11 -  | the None = raise OPTION "the";
    1.12 +  | the None = raise OPTION;
    1.13  
    1.14  fun if_none None y = y
    1.15    | if_none (Some x) _ = x;
    1.16 @@ -78,6 +78,12 @@
    1.17    | merge_opts _ (None, some as Some _) = some
    1.18    | merge_opts merge (Some x, Some y) = Some (merge (x, y));
    1.19  
    1.20 +(*handle partial functions*)
    1.21 +fun try f x = Some (f x) handle _ => None;
    1.22 +fun can f x = is_some (try f x);
    1.23 +
    1.24 +
    1.25 +
    1.26  (** pairs **)
    1.27  
    1.28  fun pair x y = (x, y);