--- a/src/Pure/library.ML Thu Dec 22 00:28:43 2005 +0100
+++ b/src/Pure/library.ML Thu Dec 22 00:28:44 2005 +0100
@@ -546,9 +546,11 @@
| dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
(*return nth element of a list, where 0 designates the first element;
- raise EXCEPTION if list too short*)
+ raise Subscript if list too short*)
fun nth xs i = List.nth (xs, i);
+fun nth_list xss i = nth xss i handle Subscript => [];
+
(*update nth element*)
fun nth_update (n, x) xs =
(case splitAt (n, xs) of
@@ -559,8 +561,6 @@
| nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
| nth_map _ _ [] = raise Subscript;
-fun nth_list xss i = nth xss i handle Subscript => [];
-
val last_elem = List.last;
(*rear decomposition*)