# HG changeset patch
# User haftmann
# Date 1121688611 -7200
# Node ID bc98da5727be7a089beed2881e01042cfbea4bfe
# Parent  eaafda56b14c4d856a9b5a703e0cc8b4cf6fd403
reverted from fold_yield to fold_map

diff -r eaafda56b14c -r bc98da5727be CONTRIBUTORS
--- 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.
diff -r eaafda56b14c -r bc98da5727be NEWS
--- 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 =
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 =