src/Pure/library.ML
changeset 18359 02a830bab542
parent 18333 b356f7837921
child 18376 2ef0183fa20b
     1.1 --- a/src/Pure/library.ML	Tue Dec 06 09:04:09 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Dec 06 16:07:10 2005 +0100
     1.3 @@ -101,6 +101,7 @@
     1.4    val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.5    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.6    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     1.7 +  val dig: ('a list -> 'a list) -> 'a list list -> 'a list list
     1.8    val unflat: 'a list list -> 'b list -> 'b list list
     1.9    val splitAt: int * 'a list -> 'a list * 'a list
    1.10    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    1.11 @@ -597,6 +598,10 @@
    1.12    | unflat [] [] = []
    1.13    | unflat _ _ = raise UnequalLengths;
    1.14  
    1.15 +fun dig f xss =
    1.16 +  unflat xss ((f o flat) xss);
    1.17 +
    1.18 +
    1.19  (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
    1.20    (proc x1; ...; proc xn) for side effects*)
    1.21  val seq = List.app;