--- a/src/Pure/library.ML Wed Dec 21 12:06:08 2005 +0100
+++ b/src/Pure/library.ML Wed Dec 21 13:25:20 2005 +0100
@@ -102,7 +102,7 @@
val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
- val unflat: 'a list list -> 'b list -> 'b list list
+ val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
val splitAt: int * 'a list -> 'a list * 'a list
val dropwhile: ('a -> bool) -> 'a list -> 'a list
val nth: 'a list -> int -> 'a
@@ -599,6 +599,8 @@
fun burrow f xss =
unflat xss ((f o flat) xss);
+fun burrow_split f xss =
+ apsnd (unflat xss) ((f o flat) xss);
(*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
(proc x1; ...; proc xn) for side effects*)