# HG changeset patch
# User wenzelm
# Date 1135207724 -3600
# Node ID 9125d278fdc805ad55848b6720880ebe6c398046
# Parent  9a1458cb295618f703bcdf714331faa72f8732b9
tuned;

diff -r 9a1458cb2956 -r 9125d278fdc8 src/HOL/Induct/Term.thy
--- 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)
diff -r 9a1458cb2956 -r 9125d278fdc8 src/Pure/library.ML
--- 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*)