added map_option;

--- 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;