# HG changeset patch
# User wenzelm
# Date 1003170678 -7200
# Node ID 983d2db52062a0ae53f4fba3c4aad9eeae213aa1
# Parent  cf618fe8facdd81e79101c934e944dfa46d27e8f
map_nth_elem;

diff -r cf618fe8facd -r 983d2db52062 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Oct 15 17:02:57 2001 +0200
+++ b/src/Pure/library.ML	Mon Oct 15 20:31:18 2001 +0200
@@ -91,6 +91,7 @@
   val drop: int * 'a list -> 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
   val nth_elem: int * 'a list -> 'a
+  val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list
   val last_elem: 'a list -> 'a
   val split_last: 'a list -> 'a list * 'a
   val nth_update: 'a -> int * 'a list -> 'a list
@@ -508,6 +509,10 @@
     [] => raise LIST "nth_elem"
   | x :: _ => x);
 
+fun map_nth_elem 0 f (x :: xs) = f x :: xs
+  | map_nth_elem n f (x :: xs) = x :: map_nth_elem (n - 1) f xs
+  | map_nth_elem _ _ [] = raise LIST "map_nth_elem";
+
 (*last element of a list*)
 fun last_elem [] = raise LIST "last_elem"
   | last_elem [x] = x