# HG changeset patch
# User haftmann
# Date 1191520487 -7200
# Node ID d8ff870a11ff37d10a4b0fecbbea5f9ca6a6b476
# Parent  abcd15369ffa7e7cddad4c668739c3e4dd512a63
added nth_drop

diff -r abcd15369ffa -r d8ff870a11ff src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Oct 04 19:54:46 2007 +0200
+++ b/src/Pure/library.ML	Thu Oct 04 19:54:47 2007 +0200
@@ -84,6 +84,7 @@
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
   val nth: 'a list -> int -> 'a
   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
+  val nth_drop: int -> '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
@@ -433,6 +434,9 @@
   | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
   | nth_map (_: int) _ [] = raise Subscript;
 
+fun nth_drop n xs =
+  List.take (xs, n) @ List.drop (xs, n + 1);
+
 fun map_index f =
   let
     fun mapp (_: int) [] = []