added map_index

--- a/src/Pure/library.ML	Fri Dec 23 20:02:30 2005 +0100
+++ b/src/Pure/library.ML	Tue Dec 27 15:24:23 2005 +0100
@@ -98,7 +98,6 @@
   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
-  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
@@ -109,6 +108,8 @@
   val nth_update: int * 'a -> 'a list -> 'a list
   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   val nth_list: 'a list list -> int -> 'a list
+  val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
+  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val split_last: 'a list -> 'a list * 'a
   val find_index: ('a -> bool) -> 'a list -> int
   val find_index_eq: ''a -> ''a list -> int
@@ -510,7 +511,7 @@
 
 fun fold_index f =
   let
-    fun fold_aux _  [] y = y
+    fun fold_aux _ [] y = y
       | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
   in fold_aux 0 end;
 
@@ -561,6 +562,12 @@
   | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
   | nth_map _ _ [] = raise Subscript;
 
+fun map_index f =
+  let
+    fun mapp _ [] = []
+      | mapp i (x :: xs) = f (i, x) :: mapp (i+1) xs
+  in mapp 0 end;
+
 val last_elem = List.last;
 
 (*rear decomposition*)