--- a/src/HOL/Induct/Term.thy Thu Dec 22 00:28:43 2005 +0100
+++ b/src/HOL/Induct/Term.thy Thu Dec 22 00:28:44 2005 +0100
@@ -44,7 +44,7 @@
assumes var: "!!v. P (Var v)"
and app: "!!f ts. list_all P ts ==> P (App f ts)"
shows term_induct2: "P t"
-and "list_all P ts"
+ and "list_all P ts"
apply (induct t and ts)
apply (rule var)
apply (rule app)
--- 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*)