# HG changeset patch
# User wenzelm
# Date 894308738 -7200
# Node ID df9d6eef16d5512057ff7981f6ec6bedda761b59
# Parent  0f80e924009d50bb8d9e3183550f379f662522dd
added nth_update: 'a -> int * 'a list -> 'a list;

diff -r 0f80e924009d -r df9d6eef16d5 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon May 04 21:05:14 1998 +0200
+++ b/src/Pure/library.ML	Mon May 04 21:05:38 1998 +0200
@@ -80,6 +80,7 @@
   val nth_elem: int * 'a list -> 'a
   val last_elem: 'a list -> 'a
   val split_last: 'a list -> 'a list * 'a
+  val nth_update: 'a -> int * 'a list -> 'a list
   val find_index: ('a -> bool) -> 'a list -> int
   val find_index_eq: ''a -> ''a list -> int
   val find_first: ('a -> bool) -> 'a list -> 'a option
@@ -446,6 +447,17 @@
   | split_last [x] = ([], x)
   | split_last (x :: xs) = apfst (cons x) (split_last xs);
 
+(*update nth element*)
+fun nth_update x (n, xs) =
+  let
+    val prfx = take (n, xs);
+    val sffx = drop (n, xs);
+  in
+    (case sffx of
+      [] => raise LIST "nth_update"
+    | _ :: sffx' => prfx @ (x :: sffx'))
+  end;
+
 (*find the position of an element in a list*)
 fun find_index pred =
   let fun find _ [] = ~1