src/Pure/library.ML

   val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
   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
   val nth: 'a list -> int -> 'a
   val nth_update: int * 'a -> 'a list -> 'a list

       let val (ps,qs) = splitAt(length xs,ys)
       in ps :: unflat xss qs end
   | 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;
 
 (*separate s [x1, x2, ..., xn]  ===>  [x1, s, x2, s, ..., s, xn]*)