--- a/src/Pure/General/same.ML Thu Jul 16 17:03:11 2009 +0200
+++ b/src/Pure/General/same.ML Thu Jul 16 20:15:57 2009 +0200
@@ -13,6 +13,7 @@
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 =
@@ -32,5 +33,7 @@
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;