--- 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 =
--- 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);
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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,
--- 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
--- 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
--- 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')
--- 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);
--- 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 " ^
--- 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;
--- 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;
--- 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))
--- 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;
--- 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
--- 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) =
--- 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) =>
--- 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)
--- 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 *)
--- 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)
--- 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;
--- 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