# HG changeset patch
# User haftmann
# Date 1201039644 -3600
# Node ID d431d65346a1789829723a3a5b5b46529779bc32
# Parent  a52309ac4a4da39046e6444bb178f7b53969ebf2
added map_split

diff -r a52309ac4a4d -r d431d65346a1 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jan 22 23:07:21 2008 +0100
+++ b/src/Pure/library.ML	Tue Jan 22 23:07:24 2008 +0100
@@ -107,6 +107,7 @@
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   val ~~ : 'a list * 'b list -> ('a * 'b) list
+  val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
   val split_list: ('a * 'b) list -> 'a list * 'b list
   val separate: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
@@ -573,6 +574,13 @@
   | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
   | fold2 f _ _ _ = raise UnequalLengths;
 
+fun map_split f [] = ([], [])
+  | map_split f (x :: xs) =
+      let
+        val (y, w) = f x;
+        val (ys, ws) = map_split f xs;
+      in (y :: ys, w :: ws) end;
+
 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
   | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
   | zip_options _ [] = []