src/Pure/library.ML
changeset 18461 9125d278fdc8
parent 18452 5ea633c9bc05
child 18514 0cec730b3942
     1.1 --- a/src/Pure/library.ML	Thu Dec 22 00:28:43 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Dec 22 00:28:44 2005 +0100
     1.3 @@ -546,9 +546,11 @@
     1.4    | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
     1.5  
     1.6  (*return nth element of a list, where 0 designates the first element;
     1.7 -  raise EXCEPTION if list too short*)
     1.8 +  raise Subscript if list too short*)
     1.9  fun nth xs i = List.nth (xs, i);
    1.10  
    1.11 +fun nth_list xss i = nth xss i handle Subscript => [];
    1.12 +
    1.13  (*update nth element*)
    1.14  fun nth_update (n, x) xs =
    1.15      (case splitAt (n, xs) of
    1.16 @@ -559,8 +561,6 @@
    1.17    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    1.18    | nth_map _ _ [] = raise Subscript;
    1.19  
    1.20 -fun nth_list xss i = nth xss i handle Subscript => [];
    1.21 -
    1.22  val last_elem = List.last;
    1.23  
    1.24  (*rear decomposition*)