# HG changeset patch
# User wenzelm
# Date 1144922462 -7200
# Node ID b701ea590259679b7b04bc931c0928ff67f99a56
# Parent  51eeee99bd8fd0ec03e0725538ae641450d31e9e
export unflat (again);

diff -r 51eeee99bd8f -r b701ea590259 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Apr 13 12:01:01 2006 +0200
+++ b/src/Pure/library.ML	Thu Apr 13 12:01:02 2006 +0200
@@ -112,6 +112,7 @@
   val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
+  val unflat: 'a list list -> 'b list -> 'b list list
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
   val chop: int -> 'a list -> 'a list * 'a list
@@ -652,7 +653,7 @@
 val flat = List.concat;
 
 fun unflat (xs :: xss) ys =
-      let val (ps,qs) = splitAt(length xs,ys)
+      let val (ps, qs) = chop (length xs) ys
       in ps :: unflat xss qs end
   | unflat [] [] = []
   | unflat _ _ = raise UnequalLengths;