# HG changeset patch
# User wenzelm
# Date 1247768157 -7200
# Node ID e91a3acf8383b3d0bb29c05b06c915e58446dfb0
# Parent  597b3b69b8d829e511d9b9cddabcda3227eb31d0
added map;

diff -r 597b3b69b8d8 -r e91a3acf8383 src/Pure/General/same.ML
--- 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;