# HG changeset patch
# User wenzelm
# Date 1133301603 -3600
# Node ID 7273cf5085ed5ab75cca90bf918a2e205721332a
# Parent  83e92f9b32c413f4439a858b192a93c2ce7f8e2f
added nth_list;

diff -r 83e92f9b32c4 -r 7273cf5085ed src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Nov 29 22:52:19 2005 +0100
+++ b/src/Pure/library.ML	Tue Nov 29 23:00:03 2005 +0100
@@ -107,6 +107,7 @@
   val nth: 'a list -> int -> 'a
   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 split_last: 'a list -> 'a list * 'a
   val find_index: ('a -> bool) -> 'a list -> int
   val find_index_eq: ''a -> ''a list -> int
@@ -563,7 +564,8 @@
   | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
   | nth_map _ _ [] = raise Subscript;
 
-(*last element of a list*)
+fun nth_list xss i = nth xss i handle Subscript => [];
+
 val last_elem = List.last;
 
 (*rear decomposition*)