reverted from fold_yield to fold_map
authorhaftmann
Mon Jul 18 14:10:11 2005 +0200 (2005-07-18)
changeset 16869bc98da5727be
parent 16868 eaafda56b14c
child 16870 a1155e140597
reverted from fold_yield to fold_map
CONTRIBUTORS
NEWS
src/Pure/library.ML
     1.1 --- a/CONTRIBUTORS	Fri Jul 15 15:45:04 2005 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Jul 18 14:10:11 2005 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  
     1.5  * July 2005: Florian Haftmann, TUM
     1.6    Some combinators for linear functional transformations in ML:
     1.7 -  |->  #->  fold_yield  etc.
     1.8 +  |->  #->  fold_map  etc.
     1.9  
    1.10  * May 2005: Rafal Kolanski, NICTA
    1.11    Substantially improved retrieval of facts from theory/proof context.
     2.1 --- a/NEWS	Fri Jul 15 15:45:04 2005 +0200
     2.2 +++ b/NEWS	Mon Jul 18 14:10:11 2005 +0200
     2.3 @@ -402,7 +402,7 @@
     2.4    (x, y) |-> f		f #-> g
     2.5  
     2.6  * Pure/library.ML: canonical list combinators fold, fold_rev, and
     2.7 -fold_yield support linear functional transformations and nesting.  For
     2.8 +fold_map support linear functional transformations and nesting.  For
     2.9  example:
    2.10  
    2.11    fold f [x1, ..., xN] y =
     3.1 --- a/src/Pure/library.ML	Fri Jul 15 15:45:04 2005 +0200
     3.2 +++ b/src/Pure/library.ML	Mon Jul 18 14:10:11 2005 +0200
     3.3 @@ -91,7 +91,7 @@
     3.4    val apply: ('a -> 'a) list -> 'a -> 'a
     3.5    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     3.6    val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     3.7 -  val fold_yield: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     3.8 +  val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     3.9    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    3.10    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    3.11    val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
    3.12 @@ -479,7 +479,7 @@
    3.13        | fold_aux (x :: xs) y = f x (fold_aux xs y);
    3.14    in fold_aux end;
    3.15  
    3.16 -fun fold_yield f =
    3.17 +fun fold_map f =
    3.18    let
    3.19      fun fold_aux [] y = ([], y)
    3.20        | fold_aux (x :: xs) y =