tuned;
authorwenzelm
Thu Dec 22 00:28:44 2005 +0100 (2005-12-22)
changeset 184619125d278fdc8
parent 18460 9a1458cb2956
child 18462 b67d423b5234
tuned;
src/HOL/Induct/Term.thy
src/Pure/library.ML
     1.1 --- a/src/HOL/Induct/Term.thy	Thu Dec 22 00:28:43 2005 +0100
     1.2 +++ b/src/HOL/Induct/Term.thy	Thu Dec 22 00:28:44 2005 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4    assumes var: "!!v. P (Var v)"
     1.5      and app: "!!f ts. list_all P ts ==> P (App f ts)"
     1.6    shows term_induct2: "P t"
     1.7 -and "list_all P ts"
     1.8 +    and "list_all P ts"
     1.9    apply (induct t and ts)
    1.10       apply (rule var)
    1.11      apply (rule app)
     2.1 --- a/src/Pure/library.ML	Thu Dec 22 00:28:43 2005 +0100
     2.2 +++ b/src/Pure/library.ML	Thu Dec 22 00:28:44 2005 +0100
     2.3 @@ -546,9 +546,11 @@
     2.4    | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
     2.5  
     2.6  (*return nth element of a list, where 0 designates the first element;
     2.7 -  raise EXCEPTION if list too short*)
     2.8 +  raise Subscript if list too short*)
     2.9  fun nth xs i = List.nth (xs, i);
    2.10  
    2.11 +fun nth_list xss i = nth xss i handle Subscript => [];
    2.12 +
    2.13  (*update nth element*)
    2.14  fun nth_update (n, x) xs =
    2.15      (case splitAt (n, xs) of
    2.16 @@ -559,8 +561,6 @@
    2.17    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    2.18    | nth_map _ _ [] = raise Subscript;
    2.19  
    2.20 -fun nth_list xss i = nth xss i handle Subscript => [];
    2.21 -
    2.22  val last_elem = List.last;
    2.23  
    2.24  (*rear decomposition*)