# HG changeset patch
# User wenzelm
# Date 1005510631 -3600
# Node ID 74156e7bb22ef4325eebccec2387812fdd715c62
# Parent  e370e5d469c26130fbf059ac0ed51358fd0f0f2f
added unflat;

diff -r e370e5d469c2 -r 74156e7bb22e src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Nov 11 21:30:10 2001 +0100
+++ b/src/Pure/library.ML	Sun Nov 11 21:30:31 2001 +0100
@@ -101,6 +101,7 @@
   val find_first: ('a -> bool) -> 'a list -> 'a option
   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   val flat: 'a list list -> 'a list
+  val unflat: 'a list list -> 'b list -> 'b list list
   val seq: ('a -> unit) -> 'a list -> unit
   val separate: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
@@ -564,6 +565,11 @@
 (*flatten a list of lists to a list*)
 fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
 
+fun unflat (xs :: xss) ys =
+      let val n = length xs in take (n, ys) :: unflat xss (drop (n, ys)) end
+  | unflat [] [] = []
+  | unflat _ _ = raise LIST "unflat";
+
 (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
   (proc x1; ...; proc xn) for side effects*)
 fun seq (proc: 'a -> unit) : 'a list -> unit =