1.1 --- a/src/Pure/library.ML	Thu Oct 04 19:54:46 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Oct 04 19:54:47 2007 +0200
     1.3 @@ -84,6 +84,7 @@
     1.4    val dropwhile: ('a -> bool) -> 'a list -> 'a list
     1.5    val nth: 'a list -> int -> 'a
     1.6    val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
     1.7 +  val nth_drop: int -> 'a list -> 'a list
     1.8    val nth_list: 'a list list -> int -> 'a list
     1.9    val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
    1.10    val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.11 @@ -433,6 +434,9 @@
    1.12    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    1.13    | nth_map (_: int) _ [] = raise Subscript;
    1.14  
    1.15 +fun nth_drop n xs =
    1.16 +  List.take (xs, n) @ List.drop (xs, n + 1);
    1.17 +
    1.18  fun map_index f =
    1.19    let
    1.20      fun mapp (_: int) [] = []