added map_option;
authorwenzelm
Thu Jul 16 21:28:39 2009 +0200 (2009-07-16 ago)
changeset 32022c2f4ee07647f
parent 32021 d7f58d97fa96
child 32023 2d071ac5032f
added map_option;
src/Pure/General/same.ML
     1.1 --- a/src/Pure/General/same.ML	Thu Jul 16 21:28:09 2009 +0200
     1.2 +++ b/src/Pure/General/same.ML	Thu Jul 16 21:28:39 2009 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val function: ('a -> 'b option) -> ('a, 'b) function
     1.5    val capture: ('a, 'b) function -> 'a -> 'b option
     1.6    val map: 'a operation -> 'a list operation
     1.7 +  val map_option: ('a, 'b) function -> ('a option, 'b option) function
     1.8  end;
     1.9  
    1.10  structure Same: SAME =
    1.11 @@ -36,4 +37,7 @@
    1.12  fun map f [] = raise SAME
    1.13    | map f (x :: xs) = (f x :: commit (map f) xs handle SAME => x :: map f xs);
    1.14  
    1.15 +fun map_option f NONE = raise SAME
    1.16 +  | map_option f (SOME x) = SOME (f x);
    1.17 +
    1.18  end;