# HG changeset patch
# User haftmann
# Date 1369985432 -7200
# Node ID 6f3771c00280ac94aee88d97593880d5f9070ec3
# Parent  19bd34e97e2e826f85ca113de1e35d3423c23848
combinator fold_range, corresponding to map_range

diff -r 19bd34e97e2e -r 6f3771c00280 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri May 31 07:55:40 2013 +0200
+++ b/src/Pure/library.ML	Fri May 31 09:30:32 2013 +0200
@@ -82,6 +82,7 @@
   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val map_range: (int -> 'a) -> int -> 'a list
+  val fold_range: (int -> 'a -> 'a) -> int -> 'a -> 'a
   val split_last: 'a list -> 'a list * 'a
   val find_first: ('a -> bool) -> 'a list -> 'a option
   val find_index: ('a -> bool) -> 'a list -> int
@@ -430,21 +431,28 @@
 
 fun map_index f =
   let
-    fun mapp (_: int) [] = []
-      | mapp i (x :: xs) = f (i, x) :: mapp (i + 1) xs
-  in mapp 0 end;
+    fun map_aux (_: int) [] = []
+      | map_aux i (x :: xs) = f (i, x) :: map_aux (i + 1) xs
+  in map_aux 0 end;
 
 fun fold_index f =
   let
     fun fold_aux (_: int) [] y = y
-      | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y);
+      | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y)
   in fold_aux 0 end;
 
 fun map_range f i =
   let
-    fun mapp (k: int) =
-      if k < i then f k :: mapp (k + 1) else [];
-  in mapp 0 end;
+    fun map_aux (k: int) =
+      if k < i then f k :: map_aux (k + 1) else []
+  in map_aux 0 end;
+
+fun fold_range f i =
+  let
+    fun fold_aux (k: int) y =
+      if k < i then fold_aux (k + 1) (f k y) else y
+  in fold_aux 0 end;
+
 
 (*rear decomposition*)
 fun split_last [] = raise List.Empty