src/Pure/library.ML
changeset 18286 7273cf5085ed
parent 18278 cbf6f44d73d3
child 18330 444f16d232a2
     1.1 --- a/src/Pure/library.ML	Tue Nov 29 22:52:19 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Nov 29 23:00:03 2005 +0100
     1.3 @@ -107,6 +107,7 @@
     1.4    val nth: 'a list -> int -> 'a
     1.5    val nth_update: int * 'a -> 'a list -> 'a list
     1.6    val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
     1.7 +  val nth_list: 'a list list -> int -> 'a list
     1.8    val split_last: 'a list -> 'a list * 'a
     1.9    val find_index: ('a -> bool) -> 'a list -> int
    1.10    val find_index_eq: ''a -> ''a list -> int
    1.11 @@ -563,7 +564,8 @@
    1.12    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    1.13    | nth_map _ _ [] = raise Subscript;
    1.14  
    1.15 -(*last element of a list*)
    1.16 +fun nth_list xss i = nth xss i handle Subscript => [];
    1.17 +
    1.18  val last_elem = List.last;
    1.19  
    1.20  (*rear decomposition*)