1.1 --- a/src/Pure/library.ML	Fri Jul 15 15:45:04 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Jul 18 14:10:11 2005 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4    val apply: ('a -> 'a) list -> 'a -> 'a
     1.5    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.6    val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.7 -  val fold_yield: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     1.8 +  val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     1.9    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.10    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.11    val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.12 @@ -479,7 +479,7 @@
    1.13        | fold_aux (x :: xs) y = f x (fold_aux xs y);
    1.14    in fold_aux end;
    1.15  
    1.16 -fun fold_yield f =
    1.17 +fun fold_map f =
    1.18    let
    1.19      fun fold_aux [] y = ([], y)
    1.20        | fold_aux (x :: xs) y =