standardized split_last/last_elem towards List.last;
eliminated obsolete Library.last_elem;

--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -1207,7 +1207,7 @@
     val ind_prems' =
       map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
         HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
-          (snd (split_last (binder_types T)) --> HOLogic.boolT) -->
+          (List.last (binder_types T) --> HOLogic.boolT) -->
             HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
       maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
         map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $

--- a/src/HOL/Nominal/nominal_permeq.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -302,7 +302,7 @@
               vs HOLogic.unit;
             val s' = list_abs (ps,
               Const ("Nominal.supp", fastype_of1 (Ts, s) -->
-                snd (split_last (binder_types T)) --> HOLogic.boolT) $ s);
+                List.last (binder_types T) --> HOLogic.boolT) $ s);
             val supports_rule' = Thm.lift_rule goal supports_rule;
             val _ $ (_ $ S $ _) =
               Logic.strip_assums_concl (hd (prems_of supports_rule'));

--- a/src/HOL/Nominal/nominal_primrec.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -324,7 +324,7 @@
         val (i, j, cargs) = mk_idx eq
         val th = nth (nth rec_rewritess i) j;
         val cargs' = th |> concl_of |> HOLogic.dest_Trueprop |>
-          HOLogic.dest_eq |> fst |> strip_comb |> snd |> split_last |> snd |>
+          HOLogic.dest_eq |> fst |> strip_comb |> snd |> List.last |>
           strip_comb |> snd
       in (cargs, Logic.strip_imp_prems eq,
         Drule.cterm_instantiate (inst @

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -71,8 +71,9 @@
   let
     val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
     val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
-    val default = if null tab then NONE
-      else SOME (snd (Library.last_elem tab))
+    val default =
+      if null tab then NONE
+      else SOME (snd (List.last tab))
         (*conservative wrt. overloaded constructors*);
   in case hint
    of NONE => default

--- a/src/HOL/Tools/inductive_codegen.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -62,14 +62,17 @@
         let
           val cs = fold Term.add_const_names (Thm.prems_of thm) [];
           val rules = Symtab.lookup_list intros s;
-          val nparms = (case optnparms of
-            SOME k => k
-          | NONE => (case rules of
-             [] => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
-                 SOME (_, {raw_induct, ...}) =>
-                   length (Inductive.params_of raw_induct)
-               | NONE => 0)
-            | xs => snd (snd (snd (split_last xs)))))
+          val nparms =
+            (case optnparms of
+              SOME k => k
+            | NONE =>
+                (case rules of
+                  [] =>
+                    (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
+                      SOME (_, {raw_induct, ...}) =>
+                        length (Inductive.params_of raw_induct)
+                    | NONE => 0)
+                | xs => snd (snd (List.last xs))))
         in CodegenData.put
           {intros = intros |>
            Symtab.update (s, (AList.update Thm.eq_thm_prop

--- a/src/HOL/Tools/inductive_set.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -242,7 +242,7 @@
         NONE => thm' RS sym
       | SOME fs' =>
           let
-            val (_, U) = split_last (binder_types T);
+            val U = List.last (binder_types T);
             val Ts = HOLogic.strip_ptupleT fs' U;
             (* FIXME: should cterm_instantiate increment indexes? *)
             val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;

--- a/src/HOL/Tools/list_to_set_comprehension.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -93,8 +93,8 @@
               SOME i => 
                 let
                   val (Ts, _) = strip_type T
-                  val T' = snd (split_last Ts)
-                in SOME (snd (split_last args), T', i, nth args i) end
+                  val T' = List.last Ts
+                in SOME (List.last args, T', i, nth args i) end
             | NONE => NONE)
           | NONE => NONE)
         | NONE => NONE
@@ -111,13 +111,13 @@
       THEN rtac @{thm impI} 1
       THEN Subgoal.FOCUS (fn {prems, context, ...} =>
         CONVERSION (right_hand_set_comprehension_conv (K
-          (conj_conv (Conv.rewr_conv (snd (split_last prems) RS @{thm Eq_TrueI})) Conv.all_conv
+          (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
            then_conv rewr_conv' @{thm simp_thms(22)})) context) 1) ctxt 1
       THEN tac ctxt cont
       THEN rtac @{thm impI} 1
       THEN Subgoal.FOCUS (fn {prems, context, ...} =>
           CONVERSION (right_hand_set_comprehension_conv (K
-            (conj_conv (Conv.rewr_conv (snd (split_last prems) RS @{thm Eq_FalseI})) Conv.all_conv
+            (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
              then_conv rewr_conv' @{thm simp_thms(24)})) context) 1) ctxt 1
       THEN rtac set_Nil_I 1
     | tac ctxt (Case (T, i) :: cont) =
@@ -135,7 +135,7 @@
             Subgoal.FOCUS (fn {prems, context, ...} =>
               CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
                   ((conj_conv 
-                    (eq_conv Conv.all_conv (rewr_conv' (snd (split_last prems)))
+                    (eq_conv Conv.all_conv (rewr_conv' (List.last prems))
                     then_conv (Conv.try_conv (Conv.rewrs_conv (map meta_eq (#inject info))))) Conv.all_conv)
                     then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
                     then_conv (Conv.try_conv (rewr_conv' @{thm conj_assoc})))) context
@@ -147,7 +147,7 @@
               CONVERSION ((right_hand_set_comprehension_conv (K
                 (conj_conv
                   ((eq_conv Conv.all_conv
-                    (rewr_conv' (snd (split_last prems))))
+                    (rewr_conv' (List.last prems)))
                      then_conv (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info)))) Conv.all_conv
                   then_conv (rewr_conv' @{thm simp_thms(24)}))) context)
                then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>

--- a/src/HOL/Tools/record.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/Tools/record.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -250,8 +250,6 @@
 
 (*** utilities ***)
 
-fun but_last xs = fst (split_last xs);
-
 fun varifyT midx =
   let fun varify (a, S) = TVar ((a, midx + 1), S);
   in map_type_tfree varify end;
@@ -591,7 +589,7 @@
     val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
     val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
 
-    val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) Vartab.empty;
+    val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
     val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
   in (fields', (more, moreT)) end;
 
@@ -689,7 +687,7 @@
               (case get_extfields thy ext of
                 SOME fields =>
                   let
-                    val fields' = but_last fields;
+                    val (fields', _) = split_last fields;
                     val types = map snd fields';
                     val (args, rest) = split_args (map fst fields') fargs;
                     val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
@@ -701,7 +699,7 @@
                       handle Type.TYPE_MATCH => err "type is no proper record (extension)";
                     val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
                     val alphas' =
-                      map (term_of_typ o Envir.norm_type subst o varifyT) (but_last alphas);
+                      map (term_of_typ o Envir.norm_type subst o varifyT) (#1 (split_last alphas));
 
                     val more' = mk_ext rest;
                   in
@@ -749,7 +747,7 @@
               (case get_extfields thy ext of
                 SOME fields =>
                   let
-                    val (args, rest) = split_args (map fst (but_last fields)) fargs;
+                    val (args, rest) = split_args (map fst (fst (split_last fields))) fargs;
                     val more' = mk_ext rest;
                   in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
               | NONE => err ("no fields defined for " ^ ext))
@@ -822,11 +820,11 @@
                   (case get_fieldext thy x of
                     SOME (_, alphas) =>
                      (let
-                        val f :: fs = but_last fields;
+                        val (f :: fs, _) = split_last fields;
                         val fields' =
                           apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
                         val (args', more) = split_last args;
-                        val alphavars = map varifyT (but_last alphas);
+                        val alphavars = map varifyT (#1 (split_last alphas));
                         val subst = Type.raw_matches (alphavars, args') Vartab.empty;
                         val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
                       in fields'' @ strip_fields more end
@@ -913,7 +911,7 @@
               (case get_extfields thy ext' of
                 SOME fields =>
                  (let
-                    val f :: fs = but_last (map fst fields);
+                    val (f :: fs, _) = split_last (map fst fields);
                     val fields' = extern f :: map Long_Name.base_name fs;
                     val (args', more) = split_last args;
                   in (fields' ~~ args') @ strip_fields more end

--- a/src/HOL/ex/Numeral.thy	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/HOL/ex/Numeral.thy	Mon Jan 10 15:19:48 2011 +0100
@@ -588,7 +588,7 @@
 simproc_setup numeral_minus ("of_num m - of_num n") = {*
   let
     (*TODO proper implicit use of morphism via pattern antiquotations*)
-    fun cdest_of_num ct = (snd o split_last o snd o Drule.strip_comb) ct;
+    fun cdest_of_num ct = (List.last o snd o Drule.strip_comb) ct;
     fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n);
     fun attach_num ct = (dest_num (Thm.term_of ct), ct);
     fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;

--- a/src/Pure/Isar/auto_bind.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -44,7 +44,7 @@
 
 fun facts _ [] = []
   | facts thy props =
-      let val prop = Library.last_elem props
+      let val prop = List.last props
       in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
 
 val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];

--- a/src/Pure/Thy/thm_deps.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -20,7 +20,7 @@
     fun add_dep ("", _, _) = I
       | add_dep (name, _, PBody {thms = thms', ...}) =
           let
-            val prefix = #1 (Library.split_last (Long_Name.explode name));
+            val prefix = #1 (split_last (Long_Name.explode name));
             val session =
               (case prefix of
                 a :: _ =>

--- a/src/Pure/library.ML	Mon Jan 10 08:18:49 2011 +0100
+++ b/src/Pure/library.ML	Mon Jan 10 15:19:48 2011 +0100
@@ -225,7 +225,6 @@
   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
-  val last_elem: 'a list -> 'a
 end;
 
 structure Library: LIBRARY =
@@ -455,8 +454,6 @@
       if k < i then f k :: mapp (k + 1) else [];
   in mapp 0 end;
 
-val last_elem = List.last;
-
 (*rear decomposition*)
 fun split_last [] = raise Empty
   | split_last [x] = ([], x)