src/Pure/library.ML
changeset 18050 652c95961a8b
parent 18011 685d95c793ff
child 18148 7921f41165cf
     1.1 --- a/src/Pure/library.ML	Mon Oct 31 01:43:22 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Oct 31 16:00:15 2005 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4    val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     1.5    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     1.6    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.7 -  val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.8 +  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.9    val unflat: 'a list list -> 'b list -> 'b list list
    1.10    val splitAt: int * 'a list -> 'a list * 'a list
    1.11    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    1.12 @@ -504,7 +504,11 @@
    1.13          | itr (x::l) = f(x, itr l)
    1.14    in  itr l  end;
    1.15  
    1.16 -fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
    1.17 +fun fold_index f =
    1.18 +  let
    1.19 +    fun fold_aux _  [] y = y
    1.20 +      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
    1.21 +  in fold_aux 0 end;
    1.22  
    1.23  fun foldl_map f =
    1.24    let