# HG changeset patch # User wenzelm # Date 1294669188 -3600 # Node ID 8e2b8649507d6ab13a673fc9555e4535bdd6f604 # Parent 2110405ed53b399169fbbed2146aec5ba7211a5a standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem; diff -r 2110405ed53b -r 8e2b8649507d src/HOL/Nominal/nominal_datatype.ML --- 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 $ diff -r 2110405ed53b -r 8e2b8649507d src/HOL/Nominal/nominal_permeq.ML --- 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')); diff -r 2110405ed53b -r 8e2b8649507d src/HOL/Nominal/nominal_primrec.ML --- 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 @ diff -r 2110405ed53b -r 8e2b8649507d src/HOL/Tools/Datatype/datatype_data.ML --- 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 diff -r 2110405ed53b -r 8e2b8649507d src/HOL/Tools/inductive_codegen.ML --- 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 diff -r 2110405ed53b -r 8e2b8649507d src/HOL/Tools/inductive_set.ML --- 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; diff -r 2110405ed53b -r 8e2b8649507d src/HOL/Tools/list_to_set_comprehension.ML --- 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) => diff -r 2110405ed53b -r 8e2b8649507d src/HOL/Tools/record.ML --- 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 diff -r 2110405ed53b -r 8e2b8649507d src/HOL/ex/Numeral.thy --- 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; diff -r 2110405ed53b -r 8e2b8649507d src/Pure/Isar/auto_bind.ML --- 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)]; diff -r 2110405ed53b -r 8e2b8649507d src/Pure/Thy/thm_deps.ML --- 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 :: _ => diff -r 2110405ed53b -r 8e2b8649507d src/Pure/library.ML --- 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)