diff -r eaafda56b14c -r bc98da5727be src/Pure/library.ML --- a/src/Pure/library.ML Fri Jul 15 15:45:04 2005 +0200 +++ b/src/Pure/library.ML Mon Jul 18 14:10:11 2005 +0200 @@ -91,7 +91,7 @@ val apply: ('a -> 'a) list -> 'a -> 'a val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b - val fold_yield: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b + val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b @@ -479,7 +479,7 @@ | fold_aux (x :: xs) y = f x (fold_aux xs y); in fold_aux end; -fun fold_yield f = +fun fold_map f = let fun fold_aux [] y = ([], y) | fold_aux (x :: xs) y =