# HG changeset patch
# User wenzelm
# Date 1247772519 -7200
# Node ID c2f4ee07647f0bb3f0d570102499658fd6a5bdab
# Parent  d7f58d97fa96e5d68b69d10fe8b1fa4d3948f4ac
added map_option;

diff -r d7f58d97fa96 -r c2f4ee07647f src/Pure/General/same.ML
--- a/src/Pure/General/same.ML	Thu Jul 16 21:28:09 2009 +0200
+++ b/src/Pure/General/same.ML	Thu Jul 16 21:28:39 2009 +0200
@@ -14,6 +14,7 @@
   val function: ('a -> 'b option) -> ('a, 'b) function
   val capture: ('a, 'b) function -> 'a -> 'b option
   val map: 'a operation -> 'a list operation
+  val map_option: ('a, 'b) function -> ('a option, 'b option) function
 end;
 
 structure Same: SAME =
@@ -36,4 +37,7 @@
 fun map f [] = raise SAME
   | map f (x :: xs) = (f x :: commit (map f) xs handle SAME => x :: map f xs);
 
+fun map_option f NONE = raise SAME
+  | map_option f (SOME x) = SOME (f x);
+
 end;