src/Pure/library.ML
changeset 18333 b356f7837921
parent 18330 444f16d232a2
child 18359 02a830bab542
     1.1 --- a/src/Pure/library.ML	Fri Dec 02 16:04:29 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Dec 02 16:04:48 2005 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4    val if_none: 'a option -> 'a -> 'a
     1.5    val is_some: 'a option -> bool
     1.6    val is_none: 'a option -> bool
     1.7 +  val perhaps: ('a -> 'a option) -> 'a -> 'a
     1.8  
     1.9    exception EXCEPTION of exn * string
    1.10    exception ERROR
    1.11 @@ -339,6 +340,10 @@
    1.12  fun is_none (SOME _) = false
    1.13    | is_none NONE = true;
    1.14  
    1.15 +fun perhaps f x =
    1.16 +  case f x
    1.17 +   of NONE => x
    1.18 +    | SOME x' => x';
    1.19  
    1.20  (* exceptions *)
    1.21