--- a/CONTRIBUTORS Fri Jul 15 15:45:04 2005 +0200
+++ b/CONTRIBUTORS Mon Jul 18 14:10:11 2005 +0200
@@ -1,7 +1,7 @@
* July 2005: Florian Haftmann, TUM
Some combinators for linear functional transformations in ML:
- |-> #-> fold_yield etc.
+ |-> #-> fold_map etc.
* May 2005: Rafal Kolanski, NICTA
Substantially improved retrieval of facts from theory/proof context.
--- a/NEWS Fri Jul 15 15:45:04 2005 +0200
+++ b/NEWS Mon Jul 18 14:10:11 2005 +0200
@@ -402,7 +402,7 @@
(x, y) |-> f f #-> g
* Pure/library.ML: canonical list combinators fold, fold_rev, and
-fold_yield support linear functional transformations and nesting. For
+fold_map support linear functional transformations and nesting. For
example:
fold f [x1, ..., xN] y =
--- 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 =