src/Pure/General/same.ML

   type ('a, 'b) function = 'a -> 'b  (*exception SAME*)
   type 'a operation = ('a, 'a) function  (*exception SAME*)
   val commit: 'a operation -> 'a -> 'a
   val function: ('a -> 'b option) -> ('a, 'b) function
   val capture: ('a, 'b) function -> 'a -> 'b option
+  val map: 'a operation -> 'a list operation
 end;
 
 structure Same: SAME =
 struct
 

 fun function f x =
   (case f x of
     NONE => raise SAME
   | SOME y => y);
 
+fun map f [] = raise SAME
+  | map f (x :: xs) = (f x :: commit (map f) xs handle SAME => x :: map f xs);
 
 end;