# HG changeset patch
# User wenzelm
# Date 1089570923 -7200
# Node ID 8c57751cd43f9377ca51641e6ca0e0797792aa1b
# Parent  e1282c4b39bea79d0844d4bc0a0a8a19a51c4f5c
added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;

diff -r e1282c4b39be -r 8c57751cd43f src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Jul 11 20:34:50 2004 +0200
+++ b/src/Pure/library.ML	Sun Jul 11 20:35:23 2004 +0200
@@ -92,6 +92,7 @@
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val length: 'a list -> int
@@ -486,6 +487,7 @@
   in  itr l  end;
 
 fun fold f xs y = foldl (fn (y', x) => f x y') (y, xs);
+fun fold_rev f xs y = foldr (fn (x, y') => f x y') (xs, y);
 
 fun foldl_map _ (x, []) = (x, [])
   | foldl_map f (x, y :: ys) =