--- a/src/Pure/library.ML Tue Dec 06 09:04:09 2005 +0100
+++ b/src/Pure/library.ML Tue Dec 06 16:07:10 2005 +0100
@@ -101,6 +101,7 @@
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
+ val dig: ('a list -> 'a list) -> 'a list list -> 'a list list
val unflat: 'a list list -> 'b list -> 'b list list
val splitAt: int * 'a list -> 'a list * 'a list
val dropwhile: ('a -> bool) -> 'a list -> 'a list
@@ -597,6 +598,10 @@
| unflat [] [] = []
| unflat _ _ = raise UnequalLengths;
+fun dig f xss =
+ unflat xss ((f o flat) xss);
+
+
(*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
(proc x1; ...; proc xn) for side effects*)
val seq = List.app;