# HG changeset patch # User wenzelm # Date 1302970280 -7200 # Node ID 8c674b3b8e4488501bf868da2165c1973ff47a36 # Parent e52e3f697510a9f105d654065b63078269d9c0a2 eliminated old List.nth; tuned; diff -r e52e3f697510 -r 8c674b3b8e44 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Sat Apr 16 16:37:21 2011 +0200 +++ b/src/CCL/Wfd.thy Sat Apr 16 18:11:20 2011 +0200 @@ -443,9 +443,9 @@ val ihs = filter could_IH (Logic.strip_assums_hyp Bi) val rnames = map (fn x=> let val (a,b) = get_bno [] 0 x - in (List.nth(bvs,a),b) end) ihs + in (nth bvs a, b) end) ihs fun try_IHs [] = no_tac - | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs) + | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs) in try_IHs rnames end) fun is_rigid_prog t = diff -r e52e3f697510 -r 8c674b3b8e44 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/FOLP/simp.ML Sat Apr 16 18:11:20 2011 +0200 @@ -83,7 +83,7 @@ biresolve_tac (Net.unify_term net (lhs_of (Logic.strip_assums_concl prem))) i); -fun nth_subgoal i thm = List.nth(prems_of thm,i-1); +fun nth_subgoal i thm = nth (prems_of thm) (i - 1); fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm); @@ -422,7 +422,7 @@ let val ps = prems_of thm and ps' = prems_of thm'; val n = length(ps')-length(ps); - val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1))) + val a = length(Logic.strip_assums_hyp(nth ps (i - 1))) val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps')); in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end | NONE => (REW::ss,thm,anet,ats,cs); diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Apr 16 18:11:20 2011 +0200 @@ -3011,7 +3011,7 @@ Object_Logic.full_atomize_tac i THEN (fn st => let - val g = List.nth (cprems_of st, i - 1) + val g = nth (cprems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g) @@ -3021,7 +3021,7 @@ Object_Logic.full_atomize_tac i THEN (fn st => let - val g = List.nth (cprems_of st, i - 1) + val g = nth (cprems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g) diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Apr 16 18:11:20 2011 +0200 @@ -68,7 +68,7 @@ fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st => let - val g = List.nth (prems_of st, i - 1) + val g = nth (prems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_linz q g diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Apr 16 18:11:20 2011 +0200 @@ -93,7 +93,7 @@ THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i) THEN (fn st => let - val g = List.nth (prems_of st, i - 1) + val g = nth (prems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_mir thy q g diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Apr 16 18:11:20 2011 +0200 @@ -386,11 +386,11 @@ is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse rec_of arg <> n andalso rec_to (rec_of arg::ns) - (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) + (lazy_rec orelse is_lazy arg) (n, nth conss (rec_of arg))) ) o snd) cons fun warn (n,cons) = if rec_to [] false (n,cons) - then (warning ("domain "^List.nth(dnames,n)^" is empty!") true) + then (warning ("domain " ^ nth dnames n ^ " is empty!") true) else false in val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Import/proof_kernel.ML Sat Apr 16 18:11:20 2011 +0200 @@ -1261,7 +1261,7 @@ val th1 = (SOME (Global_Theory.get_thm thy thmname) handle ERROR _ => (case split_name thmname of - SOME (listname,idx) => (SOME (List.nth(Global_Theory.get_thms thy listname,idx-1)) + SOME (listname,idx) => (SOME (nth (Global_Theory.get_thms thy listname) (idx - 1)) handle _ => NONE) (* FIXME avoid handle _ *) | NONE => NONE)) in diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Import/shuffler.ML Sat Apr 16 18:11:20 2011 +0200 @@ -610,7 +610,7 @@ let val thy = Proof_Context.theory_of ctxt val _ = message ("Shuffling " ^ (string_of_thm st)) - val t = List.nth(prems_of st,i-1) + val t = nth (prems_of st) (i - 1) val set = set_prop thy t fun process_tac thms st = case set thms of diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Matrix/Compute_Oracle/am_interpreter.ML --- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML Sat Apr 16 18:11:20 2011 +0200 @@ -35,7 +35,7 @@ | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found") | term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found") -fun resolve_closure closures (CVar x) = (case List.nth (closures, x) of CDummy => CVar x | r => r) +fun resolve_closure closures (CVar x) = (case nth closures x of CDummy => CVar x | r => r) | resolve_closure closures (CConst c) = CConst c | resolve_closure closures (CApp (u, v)) = CApp (resolve_closure closures u, resolve_closure closures v) | resolve_closure closures (CAbs u) = CAbs (resolve_closure (CDummy::closures) u) @@ -160,7 +160,7 @@ and weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a)) | weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m)) - | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n | r => r) + | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case nth e n of CDummy => CVar n | r => r) | weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c) | weak_reduce (false, prog, stack, clos) = (case match_closure prog clos of diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Matrix/Compute_Oracle/am_sml.ML --- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML Sat Apr 16 18:11:20 2011 +0200 @@ -30,8 +30,6 @@ val list_nth = List.nth -(*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*) - val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) fun set_compiled_rewriter r = (compiled_rewriter := SOME r) diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Matrix/Compute_Oracle/compute.ML --- a/src/HOL/Matrix/Compute_Oracle/compute.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Sat Apr 16 18:11:20 2011 +0200 @@ -119,7 +119,7 @@ in fun infer_types naming encoding = let - fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v)) + fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, nth bounds v) | infer_types _ bounds _ (AbstractMachine.Const code) = let val c = the (Encode.lookup_term code encoding) @@ -605,7 +605,7 @@ fun run vars_allowed t = runprog (prog_of computer) (apply_subst vars_allowed varsubst t) in - case List.nth (prems, prem_no) of + case nth prems prem_no of Prem _ => raise Compute "evaluate_prem: no equality premise" | EqPrem (a, b, ty, _) => let @@ -648,7 +648,7 @@ fun run vars_allowed t = runprog (prog_of computer) (apply_subst vars_allowed varsubst t) val prems = prems_of_theorem th - val prem = run true (prem2term (List.nth (prems, prem_no))) + val prem = run true (prem2term (nth prems prem_no)) val concl = run false (concl_of_theorem th') in case match_aterms varsubst prem concl of diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Apr 16 18:11:20 2011 +0200 @@ -540,7 +540,7 @@ in (j + 1, j' + length Ts, case dt'' of DtRec k => list_all (map (pair "x") Us, - HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k), + HOLogic.mk_Trueprop (Free (nth rep_set_names k, T --> HOLogic.boolT) $ free')) :: prems | _ => prems, snd (fold_rev mk_abs_fun Ts (j', free)) :: ts) @@ -750,7 +750,7 @@ val descr' = [descr1, descr2]; fun partition_cargs idxs xs = map (fn (i, j) => - (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs; + (List.take (List.drop (xs, i), j), nth xs (i + j))) idxs; val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts, map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs)) @@ -783,7 +783,7 @@ fold_rev mk_abs_fun xs (case dt of DtRec k => if k < length new_type_names then - Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt --> + Const (nth rep_names k, typ_of_dtyp descr'' sorts dt --> typ_of_dtyp descr sorts dt) $ x else error "nested recursion not (yet) supported" | _ => x) :: r_args) @@ -1036,13 +1036,12 @@ fun mk_indrule_lemma (((i, _), T), U) (prems, concls) = let - val Rep_t = Const (List.nth (rep_names, i), T --> U) $ - mk_Free "x" T i; + val Rep_t = Const (nth rep_names i, T --> U) $ mk_Free "x" T i; - val Abs_t = Const (List.nth (abs_names, i), U --> T) + val Abs_t = Const (nth abs_names i, U --> T); in (prems @ [HOLogic.imp $ - (Const (List.nth (rep_set_names'', i), U --> HOLogic.boolT) $ Rep_t) $ + (Const (nth rep_set_names'' i, U --> HOLogic.boolT) $ Rep_t) $ (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) end; @@ -1147,8 +1146,7 @@ val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T))) (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs); - fun make_pred fsT i T = - Free (List.nth (pnames, i), fsT --> T --> HOLogic.boolT); + fun make_pred fsT i T = Free (nth pnames i, fsT --> T --> HOLogic.boolT); fun mk_fresh1 xs [] = [] | mk_fresh1 xs ((y as (_, T)) :: ys) = map (fn x => HOLogic.mk_Trueprop @@ -1470,15 +1468,15 @@ (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE) (partition_cargs idxs cargs ~~ frees'); val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~ - map (fn (i, _) => List.nth (rec_result_Ts, i)) recs; + map (fn (i, _) => nth rec_result_Ts i) recs; val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop - (List.nth (rec_sets', i) $ Free x $ Free y)) (recs ~~ frees''); + (nth rec_sets' i $ Free x $ Free y)) (recs ~~ frees''); val prems2 = map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop (fresh_const T (fastype_of f) $ Free p $ f)) binders) rec_fns; val prems3 = mk_fresh1 [] binders @ mk_fresh2 [] frees'; val prems4 = map (fn ((i, _), y) => - HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees''); + HOLogic.mk_Trueprop (nth rec_preds i $ Free y)) (recs ~~ frees''); val prems5 = mk_fresh3 (recs ~~ frees'') frees'; val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $ @@ -1486,7 +1484,7 @@ frees'') atomTs; val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop (fresh_const T fsT' $ Free x $ rec_ctxt)) binders; - val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees'')); + val result = list_comb (nth rec_fns l, map Free (frees @ frees'')); val result_freshs = map (fn p as (_, T) => fresh_const T (fastype_of result) $ Free p $ result) binders; val P = HOLogic.mk_Trueprop (p $ result) @@ -1496,7 +1494,7 @@ list_comb (Const (cname, Ts ---> T), map Free frees) $ result))], rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))], rec_prems' @ map (fn fr => list_all_free (frees @ frees'', - Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems7 @ prems6 @ [P], + Logic.list_implies (nth prems2 l @ prems3 @ prems5 @ prems7 @ prems6 @ [P], HOLogic.mk_Trueprop fr))) result_freshs, rec_eq_prems @ [flat prems2 @ prems3], l + 1) @@ -1859,7 +1857,7 @@ let val U as Type (_, [Type (_, [T, _])]) = fastype_of p; val l = find_index (equal T) dt_atomTs; - val th = List.nth (List.nth (rec_equiv_thms', l), k); + val th = nth (nth rec_equiv_thms' l) k; val th' = Thm.instantiate ([], [(cterm_of thy11 (Var (("pi", 0), U)), cterm_of thy11 p)]) th; @@ -1913,9 +1911,9 @@ Goal.prove context'' [] [] (HOLogic.mk_Trueprop (fresh_const aT T $ a $ y)) (fn _ => EVERY - (rtac (List.nth (List.nth (rec_fresh_thms, l), k)) 1 :: + (rtac (nth (nth rec_fresh_thms l) k) 1 :: map (fn th => rtac th 1) - (snd (List.nth (finite_thss, l))) @ + (snd (nth finite_thss l)) @ [rtac rec_prem 1, rtac ih 1, REPEAT_DETERM (resolve_tac fresh_prems 1)])) end) atoms diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat Apr 16 18:11:20 2011 +0200 @@ -55,7 +55,7 @@ val thy = theory_of_thm thm; (* the parsing function returns a qualified name, we get back the base name *) val atom_basename = Long_Name.base_name atom_name; - val goal = List.nth(prems_of thm, i-1); + val goal = nth (prems_of thm) (i - 1); val ps = Logic.strip_params goal; val Ts = rev (map snd ps); fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]); @@ -97,7 +97,7 @@ fun generate_fresh_fun_tac i thm = let - val goal = List.nth(prems_of thm, i-1); + val goal = nth (prems_of thm) (i - 1); val atom_name_opt = get_inner_fresh_fun goal; in case atom_name_opt of diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Sat Apr 16 18:11:20 2011 +0200 @@ -288,7 +288,7 @@ | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); fun finite_guess_tac_i tactical ss i st = - let val goal = List.nth(cprems_of st, i-1) + let val goal = nth (cprems_of st) (i - 1) in case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) => @@ -326,7 +326,7 @@ (* support of these free variables (op supports) the goal *) fun fresh_guess_tac_i tactical ss i st = let - val goal = List.nth(cprems_of st, i-1) + val goal = nth (cprems_of st) (i - 1) val fin_supp = dynamic_thms st ("fin_supp") val fresh_atm = dynamic_thms st ("fresh_atm") val ss1 = ss addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Proofs/Lambda/WeakNorm.thy --- a/src/HOL/Proofs/Lambda/WeakNorm.thy Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Sat Apr 16 18:11:20 2011 +0200 @@ -481,7 +481,7 @@ | term_of_dB' _ _ = error "term_of_dB: term not in normal form"; fun typing_of_term Ts e (Bound i) = - Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i))) + Norm.Var (e, nat_of_int i, dBtype_of_typ (nth Ts i)) | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of Type ("fun", [T, U]) => Norm.rtypingT_App (e, dB_of_term t, dBtype_of_typ T, dBtype_of_typ U, dB_of_term u, diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Statespace/state_space.ML Sat Apr 16 18:11:20 2011 +0200 @@ -252,7 +252,7 @@ fun solve_tac ctxt (_,i) st = let val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; - val goal = List.nth (cprems_of st,i-1); + val goal = nth (cprems_of st) (i - 1); val rule = DistinctTreeProver.distinct_implProver distinct_thm goal; in EVERY [rtac rule i] st end diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Sat Apr 16 18:11:20 2011 +0200 @@ -132,7 +132,7 @@ let val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule)); val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop - (Logic.strip_imp_concl (List.nth (prems_of st, i - 1)))); + (Logic.strip_imp_concl (nth (prems_of st) (i - 1)))); val getP = if can HOLogic.dest_imp (hd ts) then (apfst SOME) o HOLogic.dest_imp else pair NONE; val flt = if null indnames then I else diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Sat Apr 16 18:11:20 2011 +0200 @@ -122,7 +122,7 @@ fun make_pred i T = let val T' = T --> HOLogic.boolT - in Free (List.nth (pnames, i), T') end; + in Free (nth pnames i, T') end; fun make_ind_prem k T (cname, cargs) = let @@ -199,11 +199,10 @@ val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts); fun mk_argT (dt, T) = - binder_types T ---> List.nth (rec_result_Ts, Datatype_Aux.body_index dt); + binder_types T ---> nth rec_result_Ts (Datatype_Aux.body_index dt); val argTs = Ts @ map mk_argT recs - in argTs ---> List.nth (rec_result_Ts, i) - end) constrs) descr'; + in argTs ---> nth rec_result_Ts i end) constrs) descr'; in (rec_result_Ts, reccomb_fn_Ts) end; @@ -238,9 +237,9 @@ val frees' = map Free (rec_tnames ~~ recTs'); fun mk_reccomb ((dt, T), t) = - let val (Us, U) = strip_type T - in list_abs (map (pair "x") Us, - List.nth (reccombs, Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us)) + let val (Us, U) = strip_type T in + list_abs (map (pair "x") Us, + nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us)) end; val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees') diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Apr 16 18:11:20 2011 +0200 @@ -40,8 +40,8 @@ fun make_pred i T U r x = if member (op =) is i then - Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x - else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x; + Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x + else Free (nth pnames i, U --> HOLogic.boolT) $ x; fun mk_all i s T t = if member (op =) is i then list_all_free ([(s, T)], t) else t; @@ -117,7 +117,7 @@ |> Drule.export_without_context; val ind_name = Thm.derivation_name induct; - val vs = map (fn i => List.nth (pnames, i)) is; + val vs = map (nth pnames) is; val (thm', thy') = thy |> Sign.root_path |> Global_Theory.store_thm @@ -172,7 +172,7 @@ end; val SOME (_, _, constrs) = AList.lookup (op =) descr index; - val T = List.nth (Datatype_Aux.get_rec_types descr sorts, index); + val T = nth (Datatype_Aux.get_rec_types descr sorts) index; val (rs, prems) = split_list (map (make_casedist_prem T) constrs); val r = Const (case_name, map fastype_of rs ---> T --> rT); diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Apr 16 18:11:20 2011 +0200 @@ -466,7 +466,7 @@ let val (tm1,args) = strip_comb tm val adjustment = get_ty_arg_size thy tm1 val p' = if adjustment > p then p else p-adjustment - val tm_p = List.nth(args,p') + val tm_p = nth args p' handle Subscript => error ("Cannot replay Metis proof in Isabelle:\n" ^ "equality_inf: " ^ string_of_int p ^ " adj " ^ diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Sat Apr 16 18:11:20 2011 +0200 @@ -132,35 +132,35 @@ fun splitto splitths genth = let val _ = not (null splitths) orelse error "splitto: no given splitths"; - val sgn = Thm.theory_of_thm genth; + val thy = Thm.theory_of_thm genth; (* check if we are a member of splitths - FIXME: quicker and more flexible with discrim net. *) fun solve_by_splitth th split = - Thm.biresolution false [(false,split)] 1 th; + Thm.biresolution false [(false,split)] 1 th; fun split th = - (case find_thms_split splitths 1 th of - NONE => - (writeln (cat_lines - (["th:", Display.string_of_thm_without_context th, "split ths:"] @ - map Display.string_of_thm_without_context splitths @ ["\n--"])); - error "splitto: cannot find variable to split on") - | SOME v => - let - val gt = HOLogic.dest_Trueprop (List.nth(Thm.prems_of th, 0)); - val split_thm = mk_casesplit_goal_thm sgn v gt; - val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm; - in - expf (map recsplitf subthms) - end) + (case find_thms_split splitths 1 th of + NONE => + (writeln (cat_lines + (["th:", Display.string_of_thm_without_context th, "split ths:"] @ + map Display.string_of_thm_without_context splitths @ ["\n--"])); + error "splitto: cannot find variable to split on") + | SOME v => + let + val gt = HOLogic.dest_Trueprop (nth (Thm.prems_of th) 0); + val split_thm = mk_casesplit_goal_thm thy v gt; + val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm; + in + expf (map recsplitf subthms) + end) and recsplitf th = - (* note: multiple unifiers! we only take the first element, - probably fine -- there is probably only one anyway. *) - (case Library.get_first (Seq.pull o solve_by_splitth th) splitths of - NONE => split th - | SOME (solved_th, more) => solved_th) + (* note: multiple unifiers! we only take the first element, + probably fine -- there is probably only one anyway. *) + (case get_first (Seq.pull o solve_by_splitth th) splitths of + NONE => split th + | SOME (solved_th, more) => solved_th); in recsplitf genth end; diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/inductive.ML Sat Apr 16 18:11:20 2011 +0200 @@ -621,8 +621,7 @@ let val k = length Ts; val bs = map Bound (k - 1 downto 0); - val P = list_comb (List.nth (preds, i), - map (incr_boundvars k) ys @ bs); + val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs); val Q = list_abs (mk_names "x" k ~~ Ts, HOLogic.mk_binop inductive_conj_name (list_comb (incr_boundvars k s, bs), P)) @@ -641,10 +640,11 @@ val SOME (_, i, ys, _) = dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)) - in list_all_free (Logic.strip_params r, - Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem - (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []), - HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys)))) + in + list_all_free (Logic.strip_params r, + Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem + (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []), + HOLogic.mk_Trueprop (list_comb (nth preds i, ys)))) end; val ind_prems = map mk_ind_prem intr_ts; diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/refute.ML Sat Apr 16 18:11:20 2011 +0200 @@ -1628,7 +1628,7 @@ Const (_, T) => interpret_groundterm T | Free (_, T) => interpret_groundterm T | Var (_, T) => interpret_groundterm T - | Bound i => SOME (List.nth (#bounds args, i), model, args) + | Bound i => SOME (nth (#bounds args) i, model, args) | Abs (x, T, body) => let (* create all constants of type 'T' *) @@ -2271,7 +2271,7 @@ else () (* the type of a recursion operator is *) (* [T1, ..., Tn, IDT] ---> Tresult *) - val IDT = List.nth (binder_types T, mconstrs_count) + val IDT = nth (binder_types T) mconstrs_count (* by our assumption on the order of recursion operators *) (* and datatypes, this is the index of the datatype *) (* corresponding to the given recursion operator *) @@ -2463,15 +2463,15 @@ (* find the indices of the constructor's /recursive/ *) (* arguments *) val (_, _, constrs) = the (AList.lookup (op =) descr idx) - val (_, dtyps) = List.nth (constrs, c) - val rec_dtyps_args = filter + val (_, dtyps) = nth constrs c + val rec_dtyps_args = filter (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args) (* map those indices to interpretations *) val rec_dtyps_intrs = map (fn (dtyp, arg) => let - val dT = typ_of_dtyp descr typ_assoc dtyp + val dT = typ_of_dtyp descr typ_assoc dtyp val consts = make_constants ctxt (typs, []) dT - val arg_i = List.nth (consts, arg) + val arg_i = nth consts arg in (dtyp, arg_i) end) rec_dtyps_args @@ -3104,7 +3104,7 @@ (* generate all constants *) val consts = make_constants ctxt (typs, []) dT in - print ctxt (typs, []) dT (List.nth (consts, n)) assignment + print ctxt (typs, []) dT (nth consts n) assignment end) (cargs ~~ args) in SOME (list_comb (cTerm, argsTerms)) diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/simpdata.ML Sat Apr 16 18:11:20 2011 +0200 @@ -59,8 +59,9 @@ let fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q | count_imp _ = 0; - val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) - in if j = 0 then @{thm meta_eq_to_obj_eq} + val j = count_imp (Logic.strip_assums_concl (nth (prems_of st) (i - 1))) + in + if j = 0 then @{thm meta_eq_to_obj_eq} else let val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); @@ -69,13 +70,14 @@ val aT = TFree ("'a", HOLogic.typeS); val x = Free ("x", aT); val y = Free ("y", aT) - in Goal.prove_global (Thm.theory_of_thm st) [] - [mk_simp_implies (Logic.mk_equals (x, y))] - (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) - (fn {prems, ...} => EVERY - [rewrite_goals_tac @{thms simp_implies_def}, - REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} :: - map (rewrite_rule @{thms simp_implies_def}) prems) 1)]) + in + Goal.prove_global (Thm.theory_of_thm st) [] + [mk_simp_implies (Logic.mk_equals (x, y))] + (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) + (fn {prems, ...} => EVERY + [rewrite_goals_tac @{thms simp_implies_def}, + REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} :: + map (rewrite_rule @{thms simp_implies_def}) prems) 1)]) end end; diff -r e52e3f697510 -r 8c674b3b8e44 src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/ex/svc_funcs.ML Sat Apr 16 18:11:20 2011 +0200 @@ -137,7 +137,7 @@ fun var (Free(a,T), is) = trans_var ("F_" ^ a, T, is) | var (Var((a, 0), T), is) = trans_var (a, T, is) | var (Bound i, is) = - let val (a,T) = List.nth (params, i) + let val (a,T) = nth params i in trans_var ("B_" ^ a, T, is) end | var (t $ Bound i, is) = var(t,i::is) (*removing a parameter from a Var: the bound var index will diff -r e52e3f697510 -r 8c674b3b8e44 src/Provers/blast.ML --- a/src/Provers/blast.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/Provers/blast.ML Sat Apr 16 18:11:20 2011 +0200 @@ -1252,7 +1252,7 @@ let val thy = Thm.theory_of_thm st0 val state = initialize thy val st = Conv.gconv_rule Object_Logic.atomize_prems i st0 - val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1)) + val skoprem = fromSubgoal thy (nth (prems_of st) (i - 1)) val hyps = strip_imp_prems skoprem and concl = strip_imp_concl skoprem fun cont (tacs,_,choices) = diff -r e52e3f697510 -r 8c674b3b8e44 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/Provers/hypsubst.ML Sat Apr 16 18:11:20 2011 +0200 @@ -214,21 +214,24 @@ (*Use imp_intr, comparing the old hyps with the new ones as they come out.*) fun all_imp_intr_tac hyps i = - let fun imptac (r, []) st = reverse_n_tac r i st - | imptac (r, hyp::hyps) st = - let val (hyp',_) = List.nth (prems_of st, i-1) |> - Logic.strip_assums_concl |> - Data.dest_Trueprop |> Data.dest_imp - val (r',tac) = if Pattern.aeconv (hyp,hyp') - then (r, imp_intr_tac i THEN rotate_tac ~1 i) - else (*leave affected hyps at end*) - (r+1, imp_intr_tac i) - in - case Seq.pull(tac st) of - NONE => Seq.single(st) - | SOME(st',_) => imptac (r',hyps) st' - end - in imptac (0, rev hyps) end; + let + fun imptac (r, []) st = reverse_n_tac r i st + | imptac (r, hyp::hyps) st = + let + val (hyp', _) = + nth (prems_of st) (i - 1) + |> Logic.strip_assums_concl + |> Data.dest_Trueprop |> Data.dest_imp; + val (r', tac) = + if Pattern.aeconv (hyp, hyp') + then (r, imp_intr_tac i THEN rotate_tac ~1 i) + else (*leave affected hyps at end*) (r + 1, imp_intr_tac i); + in + (case Seq.pull (tac st) of + NONE => Seq.single st + | SOME (st', _) => imptac (r', hyps) st') + end + in imptac (0, rev hyps) end; fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) => diff -r e52e3f697510 -r 8c674b3b8e44 src/Provers/order.ML --- a/src/Provers/order.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/Provers/order.ML Sat Apr 16 18:11:20 2011 +0200 @@ -274,8 +274,9 @@ (* Internal exception, raised if contradiction ( x < x ) was derived *) fun prove asms = - let fun pr (Asm i) = List.nth (asms, i) - | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm + let + fun pr (Asm i) = nth asms i + | pr (Thm (prfs, thm)) = map pr prfs MRS thm; in pr end; (* Internal datatype for inequalities *) @@ -847,16 +848,17 @@ val v = upper edge in if (getIndex u ntc) = xi then - (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge] - @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) - else (rev_completeComponentPath u)@[edge] - @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) ) + completeTermPath x u (nth sccSubgraphs xi) @ [edge] @ + completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc)) + else + rev_completeComponentPath u @ [edge] @ + completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc)) end in - if x aconv y then - [(Le (x, y, (Thm ([], #le_refl less_thms))))] - else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi)) - else rev_completeComponentPath y ) + if x aconv y then + [(Le (x, y, (Thm ([], #le_refl less_thms))))] + else if xi = yi then completeTermPath x y (nth sccSubgraphs xi) + else rev_completeComponentPath y end; (* ******************************************************************* *) @@ -1016,15 +1018,18 @@ (* if SCC_x is linked to SCC_y via edge e *) else if ui = xi andalso vi = yi then ( case e of (Less (_, _,_)) => ( - let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) ) - val xyLesss = transPath (tl xypath, hd xypath) + let + val xypath = + completeTermPath x u (nth sccSubgraphs ui) @ [e] @ + completeTermPath v y (nth sccSubgraphs vi) + val xyLesss = transPath (tl xypath, hd xypath) in (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end) | _ => ( let - val xupath = completeTermPath x u (List.nth(sccSubgraphs, ui)) - val uxpath = completeTermPath u x (List.nth(sccSubgraphs, ui)) - val vypath = completeTermPath v y (List.nth(sccSubgraphs, vi)) - val yvpath = completeTermPath y v (List.nth(sccSubgraphs, vi)) + val xupath = completeTermPath x u (nth sccSubgraphs ui) + val uxpath = completeTermPath u x (nth sccSubgraphs ui) + val vypath = completeTermPath v y (nth sccSubgraphs vi) + val yvpath = completeTermPath y v (nth sccSubgraphs vi) val xuLesss = transPath (tl xupath, hd xupath) val uxLesss = transPath (tl uxpath, hd uxpath) val vyLesss = transPath (tl vypath, hd vypath) @@ -1037,15 +1042,18 @@ ) ) else if ui = yi andalso vi = xi then ( case e of (Less (_, _,_)) => ( - let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) ) - val xyLesss = transPath (tl xypath, hd xypath) + let + val xypath = + completeTermPath y u (nth sccSubgraphs ui) @ [e] @ + completeTermPath v x (nth sccSubgraphs vi) + val xyLesss = transPath (tl xypath, hd xypath) in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end ) | _ => ( - let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui)) - val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui)) - val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi)) - val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi)) + let val yupath = completeTermPath y u (nth sccSubgraphs ui) + val uypath = completeTermPath u y (nth sccSubgraphs ui) + val vxpath = completeTermPath v x (nth sccSubgraphs vi) + val xvpath = completeTermPath x v (nth sccSubgraphs vi) val yuLesss = transPath (tl yupath, hd yupath) val uyLesss = transPath (tl uypath, hd uypath) val vxLesss = transPath (tl vxpath, hd vxpath) diff -r e52e3f697510 -r 8c674b3b8e44 src/Provers/quasi.ML --- a/src/Provers/quasi.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/Provers/quasi.ML Sat Apr 16 18:11:20 2011 +0200 @@ -86,8 +86,9 @@ (* Internal exception, raised if contradiction ( x < x ) was derived *) fun prove asms = - let fun pr (Asm i) = List.nth (asms, i) - | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm + let + fun pr (Asm i) = nth asms i + | pr (Thm (prfs, thm)) = map pr prfs MRS thm; in pr end; (* Internal datatype for inequalities *) diff -r e52e3f697510 -r 8c674b3b8e44 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/Provers/splitter.ML Sat Apr 16 18:11:20 2011 +0200 @@ -157,7 +157,7 @@ has a body of type T; otherwise the expansion thm will fail later on *) fun type_test (T, lbnos, apsns) = - let val (_, U: typ, _) = List.nth (apsns, foldl1 Int.min lbnos) + let val (_, U: typ, _) = nth apsns (foldl1 Int.min lbnos) in T = U end; (************************************************************************* @@ -270,7 +270,7 @@ in snd (fold iter ts (0, a)) end in posns Ts [] [] t end; -fun nth_subgoal i thm = List.nth (prems_of thm, i-1); +fun nth_subgoal i thm = nth (prems_of thm) (i - 1); fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) = prod_ord (int_ord o pairself length) (order o pairself length) diff -r e52e3f697510 -r 8c674b3b8e44 src/Provers/trancl.ML --- a/src/Provers/trancl.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/Provers/trancl.ML Sat Apr 16 18:11:20 2011 +0200 @@ -95,8 +95,8 @@ fun inst thm = let val SOME (_, _, r', _) = decomp (concl_of thm) in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end; - fun pr (Asm i) = List.nth (asms, i) - | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm + fun pr (Asm i) = nth asms i + | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm; in pr end; diff -r e52e3f697510 -r 8c674b3b8e44 src/Tools/IsaPlanner/rw_tools.ML --- a/src/Tools/IsaPlanner/rw_tools.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/Tools/IsaPlanner/rw_tools.ML Sat Apr 16 18:11:20 2011 +0200 @@ -122,7 +122,7 @@ fun fake_concl_of_goal gt i = let val prems = Logic.strip_imp_prems gt - val sgt = List.nth (prems, i - 1) + val sgt = nth prems (i - 1) val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt) val tparams = Term.strip_all_vars sgt @@ -140,7 +140,7 @@ fun fake_goal gt i = let val prems = Logic.strip_imp_prems gt - val sgt = List.nth (prems, i - 1) + val sgt = nth prems (i - 1) val tbody = Term.strip_all_body sgt val tparams = Term.strip_all_vars sgt