eliminated old List.nth;
authorwenzelm
Sat Apr 16 18:11:20 2011 +0200 (2011-04-16)
changeset 423648c674b3b8e44
parent 42363 e52e3f697510
child 42365 bfd28ba57859
eliminated old List.nth;
tuned;
src/CCL/Wfd.thy
src/FOLP/simp.ML
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Matrix/Compute_Oracle/am_interpreter.ML
src/HOL/Matrix/Compute_Oracle/am_sml.ML
src/HOL/Matrix/Compute_Oracle/compute.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Proofs/Lambda/WeakNorm.thy
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/simpdata.ML
src/HOL/ex/svc_funcs.ML
src/Provers/blast.ML
src/Provers/hypsubst.ML
src/Provers/order.ML
src/Provers/quasi.ML
src/Provers/splitter.ML
src/Provers/trancl.ML
src/Tools/IsaPlanner/rw_tools.ML
     1.1 --- a/src/CCL/Wfd.thy	Sat Apr 16 16:37:21 2011 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Sat Apr 16 18:11:20 2011 +0200
     1.3 @@ -443,9 +443,9 @@
     1.4        val ihs = filter could_IH (Logic.strip_assums_hyp Bi)
     1.5        val rnames = map (fn x=>
     1.6                      let val (a,b) = get_bno [] 0 x
     1.7 -                    in (List.nth(bvs,a),b) end) ihs
     1.8 +                    in (nth bvs a, b) end) ihs
     1.9        fun try_IHs [] = no_tac
    1.10 -        | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs)
    1.11 +        | try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (nth rls (y - 1)) i ORELSE (try_IHs xs)
    1.12    in try_IHs rnames end)
    1.13  
    1.14  fun is_rigid_prog t =
     2.1 --- a/src/FOLP/simp.ML	Sat Apr 16 16:37:21 2011 +0200
     2.2 +++ b/src/FOLP/simp.ML	Sat Apr 16 18:11:20 2011 +0200
     2.3 @@ -83,7 +83,7 @@
     2.4            biresolve_tac (Net.unify_term net
     2.5                         (lhs_of (Logic.strip_assums_concl prem))) i);
     2.6  
     2.7 -fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
     2.8 +fun nth_subgoal i thm = nth (prems_of thm) (i - 1);
     2.9  
    2.10  fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm);
    2.11  
    2.12 @@ -422,7 +422,7 @@
    2.13                      let val ps = prems_of thm
    2.14                          and ps' = prems_of thm';
    2.15                          val n = length(ps')-length(ps);
    2.16 -                        val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1)))
    2.17 +                        val a = length(Logic.strip_assums_hyp(nth ps (i - 1)))
    2.18                          val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps'));
    2.19                      in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
    2.20            | NONE => (REW::ss,thm,anet,ats,cs);
     3.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 16:37:21 2011 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 18:11:20 2011 +0200
     3.3 @@ -3011,7 +3011,7 @@
     3.4   Object_Logic.full_atomize_tac i
     3.5   THEN (fn st =>
     3.6    let
     3.7 -    val g = List.nth (cprems_of st, i - 1)
     3.8 +    val g = nth (cprems_of st) (i - 1)
     3.9      val thy = Proof_Context.theory_of ctxt
    3.10      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    3.11      val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g)
    3.12 @@ -3021,7 +3021,7 @@
    3.13   Object_Logic.full_atomize_tac i
    3.14   THEN (fn st =>
    3.15    let
    3.16 -    val g = List.nth (cprems_of st, i - 1)
    3.17 +    val g = nth (cprems_of st) (i - 1)
    3.18      val thy = Proof_Context.theory_of ctxt
    3.19      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    3.20      val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g)
     4.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 16:37:21 2011 +0200
     4.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 18:11:20 2011 +0200
     4.3 @@ -68,7 +68,7 @@
     4.4  
     4.5  fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
     4.6    let
     4.7 -    val g = List.nth (prems_of st, i - 1)
     4.8 +    val g = nth (prems_of st) (i - 1)
     4.9      val thy = Proof_Context.theory_of ctxt
    4.10      (* Transform the term*)
    4.11      val (t,np,nh) = prepare_for_linz q g
     5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Apr 16 16:37:21 2011 +0200
     5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Apr 16 18:11:20 2011 +0200
     5.3 @@ -93,7 +93,7 @@
     5.4          THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
     5.5          THEN (fn st =>
     5.6    let
     5.7 -    val g = List.nth (prems_of st, i - 1)
     5.8 +    val g = nth (prems_of st) (i - 1)
     5.9      val thy = Proof_Context.theory_of ctxt
    5.10      (* Transform the term*)
    5.11      val (t,np,nh) = prepare_for_mir thy q g
     6.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Apr 16 16:37:21 2011 +0200
     6.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sat Apr 16 18:11:20 2011 +0200
     6.3 @@ -386,11 +386,11 @@
     6.4          is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
     6.5          ((rec_of arg =  n andalso not (lazy_rec orelse is_lazy arg)) orelse 
     6.6            rec_of arg <> n andalso rec_to (rec_of arg::ns) 
     6.7 -            (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
     6.8 +            (lazy_rec orelse is_lazy arg) (n, nth conss (rec_of arg)))
     6.9          ) o snd) cons
    6.10    fun warn (n,cons) =
    6.11      if rec_to [] false (n,cons)
    6.12 -    then (warning ("domain "^List.nth(dnames,n)^" is empty!") true)
    6.13 +    then (warning ("domain " ^ nth dnames n ^ " is empty!") true)
    6.14      else false
    6.15  in
    6.16    val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs
     7.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Apr 16 16:37:21 2011 +0200
     7.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Apr 16 18:11:20 2011 +0200
     7.3 @@ -1261,7 +1261,7 @@
     7.4                  val th1 = (SOME (Global_Theory.get_thm thy thmname)
     7.5                             handle ERROR _ =>
     7.6                                    (case split_name thmname of
     7.7 -                                       SOME (listname,idx) => (SOME (List.nth(Global_Theory.get_thms thy listname,idx-1))
     7.8 +                                       SOME (listname,idx) => (SOME (nth (Global_Theory.get_thms thy listname) (idx - 1))
     7.9                                                                 handle _ => NONE)  (* FIXME avoid handle _ *)
    7.10                                       | NONE => NONE))
    7.11              in
     8.1 --- a/src/HOL/Import/shuffler.ML	Sat Apr 16 16:37:21 2011 +0200
     8.2 +++ b/src/HOL/Import/shuffler.ML	Sat Apr 16 18:11:20 2011 +0200
     8.3 @@ -610,7 +610,7 @@
     8.4      let
     8.5          val thy = Proof_Context.theory_of ctxt
     8.6          val _ = message ("Shuffling " ^ (string_of_thm st))
     8.7 -        val t = List.nth(prems_of st,i-1)
     8.8 +        val t = nth (prems_of st) (i - 1)
     8.9          val set = set_prop thy t
    8.10          fun process_tac thms st =
    8.11              case set thms of
     9.1 --- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Sat Apr 16 16:37:21 2011 +0200
     9.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Sat Apr 16 18:11:20 2011 +0200
     9.3 @@ -35,7 +35,7 @@
     9.4    | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
     9.5    | term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found")
     9.6  
     9.7 -fun resolve_closure closures (CVar x) = (case List.nth (closures, x) of CDummy => CVar x | r => r)
     9.8 +fun resolve_closure closures (CVar x) = (case nth closures x of CDummy => CVar x | r => r)
     9.9    | resolve_closure closures (CConst c) = CConst c
    9.10    | resolve_closure closures (CApp (u, v)) = CApp (resolve_closure closures u, resolve_closure closures v)
    9.11    | resolve_closure closures (CAbs u) = CAbs (resolve_closure (CDummy::closures) u)
    9.12 @@ -160,7 +160,7 @@
    9.13  
    9.14  and weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a))
    9.15    | weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))
    9.16 -  | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n | r => r)
    9.17 +  | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case nth e n of CDummy => CVar n | r => r)
    9.18    | weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c)
    9.19    | weak_reduce (false, prog, stack, clos) =
    9.20      (case match_closure prog clos of
    10.1 --- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Sat Apr 16 16:37:21 2011 +0200
    10.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Sat Apr 16 18:11:20 2011 +0200
    10.3 @@ -30,8 +30,6 @@
    10.4  
    10.5  val list_nth = List.nth
    10.6  
    10.7 -(*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*)
    10.8 -
    10.9  val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
   10.10  
   10.11  fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
    11.1 --- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Sat Apr 16 16:37:21 2011 +0200
    11.2 +++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Sat Apr 16 18:11:20 2011 +0200
    11.3 @@ -119,7 +119,7 @@
    11.4  in
    11.5  fun infer_types naming encoding =
    11.6      let
    11.7 -        fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v))
    11.8 +        fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, nth bounds v)
    11.9            | infer_types _ bounds _ (AbstractMachine.Const code) = 
   11.10              let
   11.11                  val c = the (Encode.lookup_term code encoding)
   11.12 @@ -605,7 +605,7 @@
   11.13      fun run vars_allowed t = 
   11.14          runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
   11.15  in
   11.16 -    case List.nth (prems, prem_no) of
   11.17 +    case nth prems prem_no of
   11.18          Prem _ => raise Compute "evaluate_prem: no equality premise"
   11.19        | EqPrem (a, b, ty, _) =>         
   11.20          let
   11.21 @@ -648,7 +648,7 @@
   11.22      fun run vars_allowed t =
   11.23          runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
   11.24      val prems = prems_of_theorem th
   11.25 -    val prem = run true (prem2term (List.nth (prems, prem_no)))
   11.26 +    val prem = run true (prem2term (nth prems prem_no))
   11.27      val concl = run false (concl_of_theorem th')    
   11.28  in
   11.29      case match_aterms varsubst prem concl of
    12.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Apr 16 16:37:21 2011 +0200
    12.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Apr 16 18:11:20 2011 +0200
    12.3 @@ -540,7 +540,7 @@
    12.4            in (j + 1, j' + length Ts,
    12.5              case dt'' of
    12.6                  DtRec k => list_all (map (pair "x") Us,
    12.7 -                  HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
    12.8 +                  HOLogic.mk_Trueprop (Free (nth rep_set_names k,
    12.9                      T --> HOLogic.boolT) $ free')) :: prems
   12.10                | _ => prems,
   12.11              snd (fold_rev mk_abs_fun Ts (j', free)) :: ts)
   12.12 @@ -750,7 +750,7 @@
   12.13      val descr' = [descr1, descr2];
   12.14  
   12.15      fun partition_cargs idxs xs = map (fn (i, j) =>
   12.16 -      (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
   12.17 +      (List.take (List.drop (xs, i), j), nth xs (i + j))) idxs;
   12.18  
   12.19      val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts,
   12.20        map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
   12.21 @@ -783,7 +783,7 @@
   12.22               fold_rev mk_abs_fun xs
   12.23                 (case dt of
   12.24                    DtRec k => if k < length new_type_names then
   12.25 -                      Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
   12.26 +                      Const (nth rep_names k, typ_of_dtyp descr'' sorts dt -->
   12.27                          typ_of_dtyp descr sorts dt) $ x
   12.28                      else error "nested recursion not (yet) supported"
   12.29                  | _ => x) :: r_args)
   12.30 @@ -1036,13 +1036,12 @@
   12.31  
   12.32      fun mk_indrule_lemma (((i, _), T), U) (prems, concls) =
   12.33        let
   12.34 -        val Rep_t = Const (List.nth (rep_names, i), T --> U) $
   12.35 -          mk_Free "x" T i;
   12.36 +        val Rep_t = Const (nth rep_names i, T --> U) $ mk_Free "x" T i;
   12.37  
   12.38 -        val Abs_t =  Const (List.nth (abs_names, i), U --> T)
   12.39 +        val Abs_t =  Const (nth abs_names i, U --> T);
   12.40  
   12.41        in (prems @ [HOLogic.imp $
   12.42 -            (Const (List.nth (rep_set_names'', i), U --> HOLogic.boolT) $ Rep_t) $
   12.43 +            (Const (nth rep_set_names'' i, U --> HOLogic.boolT) $ Rep_t) $
   12.44                (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
   12.45            concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
   12.46        end;
   12.47 @@ -1147,8 +1146,7 @@
   12.48      val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
   12.49        (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
   12.50  
   12.51 -    fun make_pred fsT i T =
   12.52 -      Free (List.nth (pnames, i), fsT --> T --> HOLogic.boolT);
   12.53 +    fun make_pred fsT i T = Free (nth pnames i, fsT --> T --> HOLogic.boolT);
   12.54  
   12.55      fun mk_fresh1 xs [] = []
   12.56        | mk_fresh1 xs ((y as (_, T)) :: ys) = map (fn x => HOLogic.mk_Trueprop
   12.57 @@ -1470,15 +1468,15 @@
   12.58            (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
   12.59            (partition_cargs idxs cargs ~~ frees');
   12.60          val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
   12.61 -          map (fn (i, _) => List.nth (rec_result_Ts, i)) recs;
   12.62 +          map (fn (i, _) => nth rec_result_Ts i) recs;
   12.63          val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop
   12.64 -          (List.nth (rec_sets', i) $ Free x $ Free y)) (recs ~~ frees'');
   12.65 +          (nth rec_sets' i $ Free x $ Free y)) (recs ~~ frees'');
   12.66          val prems2 =
   12.67            map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop
   12.68              (fresh_const T (fastype_of f) $ Free p $ f)) binders) rec_fns;
   12.69          val prems3 = mk_fresh1 [] binders @ mk_fresh2 [] frees';
   12.70          val prems4 = map (fn ((i, _), y) =>
   12.71 -          HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
   12.72 +          HOLogic.mk_Trueprop (nth rec_preds i $ Free y)) (recs ~~ frees'');
   12.73          val prems5 = mk_fresh3 (recs ~~ frees'') frees';
   12.74          val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
   12.75            (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
   12.76 @@ -1486,7 +1484,7 @@
   12.77                 frees'') atomTs;
   12.78          val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
   12.79            (fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
   12.80 -        val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees''));
   12.81 +        val result = list_comb (nth rec_fns l, map Free (frees @ frees''));
   12.82          val result_freshs = map (fn p as (_, T) =>
   12.83            fresh_const T (fastype_of result) $ Free p $ result) binders;
   12.84          val P = HOLogic.mk_Trueprop (p $ result)
   12.85 @@ -1496,7 +1494,7 @@
   12.86               list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
   12.87           rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
   12.88           rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
   12.89 -           Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
   12.90 +           Logic.list_implies (nth prems2 l @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
   12.91               HOLogic.mk_Trueprop fr))) result_freshs,
   12.92           rec_eq_prems @ [flat prems2 @ prems3],
   12.93           l + 1)
   12.94 @@ -1859,7 +1857,7 @@
   12.95                            let
   12.96                              val U as Type (_, [Type (_, [T, _])]) = fastype_of p;
   12.97                              val l = find_index (equal T) dt_atomTs;
   12.98 -                            val th = List.nth (List.nth (rec_equiv_thms', l), k);
   12.99 +                            val th = nth (nth rec_equiv_thms' l) k;
  12.100                              val th' = Thm.instantiate ([],
  12.101                                [(cterm_of thy11 (Var (("pi", 0), U)),
  12.102                                  cterm_of thy11 p)]) th;
  12.103 @@ -1913,9 +1911,9 @@
  12.104                                Goal.prove context'' [] []
  12.105                                  (HOLogic.mk_Trueprop (fresh_const aT T $ a $ y))
  12.106                                  (fn _ => EVERY
  12.107 -                                   (rtac (List.nth (List.nth (rec_fresh_thms, l), k)) 1 ::
  12.108 +                                   (rtac (nth (nth rec_fresh_thms l) k) 1 ::
  12.109                                      map (fn th => rtac th 1)
  12.110 -                                      (snd (List.nth (finite_thss, l))) @
  12.111 +                                      (snd (nth finite_thss l)) @
  12.112                                      [rtac rec_prem 1, rtac ih 1,
  12.113                                       REPEAT_DETERM (resolve_tac fresh_prems 1)]))
  12.114                              end) atoms
    13.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Apr 16 16:37:21 2011 +0200
    13.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat Apr 16 18:11:20 2011 +0200
    13.3 @@ -55,7 +55,7 @@
    13.4     val thy = theory_of_thm thm;
    13.5  (* the parsing function returns a qualified name, we get back the base name *)
    13.6     val atom_basename = Long_Name.base_name atom_name;
    13.7 -   val goal = List.nth(prems_of thm, i-1);
    13.8 +   val goal = nth (prems_of thm) (i - 1);
    13.9     val ps = Logic.strip_params goal;
   13.10     val Ts = rev (map snd ps);
   13.11     fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
   13.12 @@ -97,7 +97,7 @@
   13.13  
   13.14  fun generate_fresh_fun_tac i thm =
   13.15    let
   13.16 -    val goal = List.nth(prems_of thm, i-1);
   13.17 +    val goal = nth (prems_of thm) (i - 1);
   13.18      val atom_name_opt = get_inner_fresh_fun goal;
   13.19    in
   13.20    case atom_name_opt of
    14.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 16 16:37:21 2011 +0200
    14.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Apr 16 18:11:20 2011 +0200
    14.3 @@ -288,7 +288,7 @@
    14.4    | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
    14.5  
    14.6  fun finite_guess_tac_i tactical ss i st =
    14.7 -    let val goal = List.nth(cprems_of st, i-1)
    14.8 +    let val goal = nth (cprems_of st) (i - 1)
    14.9      in
   14.10        case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
   14.11            _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
   14.12 @@ -326,7 +326,7 @@
   14.13  (* support of these free variables (op supports) the goal          *)
   14.14  fun fresh_guess_tac_i tactical ss i st =
   14.15      let 
   14.16 -        val goal = List.nth(cprems_of st, i-1)
   14.17 +        val goal = nth (cprems_of st) (i - 1)
   14.18          val fin_supp = dynamic_thms st ("fin_supp")
   14.19          val fresh_atm = dynamic_thms st ("fresh_atm")
   14.20          val ss1 = ss addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
    15.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Sat Apr 16 16:37:21 2011 +0200
    15.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Sat Apr 16 18:11:20 2011 +0200
    15.3 @@ -481,7 +481,7 @@
    15.4    | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
    15.5  
    15.6  fun typing_of_term Ts e (Bound i) =
    15.7 -      Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i)))
    15.8 +      Norm.Var (e, nat_of_int i, dBtype_of_typ (nth Ts i))
    15.9    | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
   15.10          Type ("fun", [T, U]) => Norm.rtypingT_App (e, dB_of_term t,
   15.11            dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
    16.1 --- a/src/HOL/Statespace/state_space.ML	Sat Apr 16 16:37:21 2011 +0200
    16.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Apr 16 18:11:20 2011 +0200
    16.3 @@ -252,7 +252,7 @@
    16.4      fun solve_tac ctxt (_,i) st =
    16.5        let
    16.6          val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name;
    16.7 -        val goal = List.nth (cprems_of st,i-1);
    16.8 +        val goal = nth (cprems_of st) (i - 1);
    16.9          val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
   16.10        in EVERY [rtac rule i] st
   16.11        end
    17.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Apr 16 16:37:21 2011 +0200
    17.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Apr 16 18:11:20 2011 +0200
    17.3 @@ -132,7 +132,7 @@
    17.4    let
    17.5      val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
    17.6      val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
    17.7 -      (Logic.strip_imp_concl (List.nth (prems_of st, i - 1))));
    17.8 +      (Logic.strip_imp_concl (nth (prems_of st) (i - 1))));
    17.9      val getP = if can HOLogic.dest_imp (hd ts) then
   17.10        (apfst SOME) o HOLogic.dest_imp else pair NONE;
   17.11      val flt = if null indnames then I else
    18.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Apr 16 16:37:21 2011 +0200
    18.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Apr 16 18:11:20 2011 +0200
    18.3 @@ -122,7 +122,7 @@
    18.4  
    18.5      fun make_pred i T =
    18.6        let val T' = T --> HOLogic.boolT
    18.7 -      in Free (List.nth (pnames, i), T') end;
    18.8 +      in Free (nth pnames i, T') end;
    18.9  
   18.10      fun make_ind_prem k T (cname, cargs) =
   18.11        let
   18.12 @@ -199,11 +199,10 @@
   18.13            val recs = filter (Datatype_Aux.is_rec_type o fst) (cargs ~~ Ts);
   18.14  
   18.15            fun mk_argT (dt, T) =
   18.16 -            binder_types T ---> List.nth (rec_result_Ts, Datatype_Aux.body_index dt);
   18.17 +            binder_types T ---> nth rec_result_Ts (Datatype_Aux.body_index dt);
   18.18  
   18.19            val argTs = Ts @ map mk_argT recs
   18.20 -        in argTs ---> List.nth (rec_result_Ts, i)
   18.21 -        end) constrs) descr';
   18.22 +        in argTs ---> nth rec_result_Ts i end) constrs) descr';
   18.23  
   18.24    in (rec_result_Ts, reccomb_fn_Ts) end;
   18.25  
   18.26 @@ -238,9 +237,9 @@
   18.27          val frees' = map Free (rec_tnames ~~ recTs');
   18.28  
   18.29          fun mk_reccomb ((dt, T), t) =
   18.30 -          let val (Us, U) = strip_type T
   18.31 -          in list_abs (map (pair "x") Us,
   18.32 -            List.nth (reccombs, Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
   18.33 +          let val (Us, U) = strip_type T in
   18.34 +            list_abs (map (pair "x") Us,
   18.35 +              nth reccombs (Datatype_Aux.body_index dt) $ Datatype_Aux.app_bnds t (length Us))
   18.36            end;
   18.37  
   18.38          val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
    19.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Apr 16 16:37:21 2011 +0200
    19.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Apr 16 18:11:20 2011 +0200
    19.3 @@ -40,8 +40,8 @@
    19.4  
    19.5      fun make_pred i T U r x =
    19.6        if member (op =) is i then
    19.7 -        Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x
    19.8 -      else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x;
    19.9 +        Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x
   19.10 +      else Free (nth pnames i, U --> HOLogic.boolT) $ x;
   19.11  
   19.12      fun mk_all i s T t =
   19.13        if member (op =) is i then list_all_free ([(s, T)], t) else t;
   19.14 @@ -117,7 +117,7 @@
   19.15        |> Drule.export_without_context;
   19.16  
   19.17      val ind_name = Thm.derivation_name induct;
   19.18 -    val vs = map (fn i => List.nth (pnames, i)) is;
   19.19 +    val vs = map (nth pnames) is;
   19.20      val (thm', thy') = thy
   19.21        |> Sign.root_path
   19.22        |> Global_Theory.store_thm
   19.23 @@ -172,7 +172,7 @@
   19.24        end;
   19.25  
   19.26      val SOME (_, _, constrs) = AList.lookup (op =) descr index;
   19.27 -    val T = List.nth (Datatype_Aux.get_rec_types descr sorts, index);
   19.28 +    val T = nth (Datatype_Aux.get_rec_types descr sorts) index;
   19.29      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
   19.30      val r = Const (case_name, map fastype_of rs ---> T --> rT);
   19.31  
    20.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Apr 16 16:37:21 2011 +0200
    20.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sat Apr 16 18:11:20 2011 +0200
    20.3 @@ -466,7 +466,7 @@
    20.4              let val (tm1,args) = strip_comb tm
    20.5                  val adjustment = get_ty_arg_size thy tm1
    20.6                  val p' = if adjustment > p then p else p-adjustment
    20.7 -                val tm_p = List.nth(args,p')
    20.8 +                val tm_p = nth args p'
    20.9                    handle Subscript =>
   20.10                           error ("Cannot replay Metis proof in Isabelle:\n" ^
   20.11                                  "equality_inf: " ^ string_of_int p ^ " adj " ^
    21.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Sat Apr 16 16:37:21 2011 +0200
    21.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Sat Apr 16 18:11:20 2011 +0200
    21.3 @@ -132,35 +132,35 @@
    21.4  fun splitto splitths genth =
    21.5      let
    21.6        val _ = not (null splitths) orelse error "splitto: no given splitths";
    21.7 -      val sgn = Thm.theory_of_thm genth;
    21.8 +      val thy = Thm.theory_of_thm genth;
    21.9  
   21.10        (* check if we are a member of splitths - FIXME: quicker and
   21.11        more flexible with discrim net. *)
   21.12        fun solve_by_splitth th split =
   21.13 -          Thm.biresolution false [(false,split)] 1 th;
   21.14 +        Thm.biresolution false [(false,split)] 1 th;
   21.15  
   21.16        fun split th =
   21.17 -          (case find_thms_split splitths 1 th of
   21.18 -             NONE =>
   21.19 -             (writeln (cat_lines
   21.20 -              (["th:", Display.string_of_thm_without_context th, "split ths:"] @
   21.21 -                map Display.string_of_thm_without_context splitths @ ["\n--"]));
   21.22 -              error "splitto: cannot find variable to split on")
   21.23 -            | SOME v =>
   21.24 -             let
   21.25 -               val gt = HOLogic.dest_Trueprop (List.nth(Thm.prems_of th, 0));
   21.26 -               val split_thm = mk_casesplit_goal_thm sgn v gt;
   21.27 -               val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
   21.28 -             in
   21.29 -               expf (map recsplitf subthms)
   21.30 -             end)
   21.31 +        (case find_thms_split splitths 1 th of
   21.32 +          NONE =>
   21.33 +           (writeln (cat_lines
   21.34 +            (["th:", Display.string_of_thm_without_context th, "split ths:"] @
   21.35 +              map Display.string_of_thm_without_context splitths @ ["\n--"]));
   21.36 +            error "splitto: cannot find variable to split on")
   21.37 +        | SOME v =>
   21.38 +            let
   21.39 +              val gt = HOLogic.dest_Trueprop (nth (Thm.prems_of th) 0);
   21.40 +              val split_thm = mk_casesplit_goal_thm thy v gt;
   21.41 +              val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
   21.42 +            in
   21.43 +              expf (map recsplitf subthms)
   21.44 +            end)
   21.45  
   21.46        and recsplitf th =
   21.47 -          (* note: multiple unifiers! we only take the first element,
   21.48 -             probably fine -- there is probably only one anyway. *)
   21.49 -          (case Library.get_first (Seq.pull o solve_by_splitth th) splitths of
   21.50 -             NONE => split th
   21.51 -           | SOME (solved_th, more) => solved_th)
   21.52 +        (* note: multiple unifiers! we only take the first element,
   21.53 +           probably fine -- there is probably only one anyway. *)
   21.54 +        (case get_first (Seq.pull o solve_by_splitth th) splitths of
   21.55 +          NONE => split th
   21.56 +        | SOME (solved_th, more) => solved_th);
   21.57      in
   21.58        recsplitf genth
   21.59      end;
    22.1 --- a/src/HOL/Tools/inductive.ML	Sat Apr 16 16:37:21 2011 +0200
    22.2 +++ b/src/HOL/Tools/inductive.ML	Sat Apr 16 18:11:20 2011 +0200
    22.3 @@ -621,8 +621,7 @@
    22.4                let
    22.5                  val k = length Ts;
    22.6                  val bs = map Bound (k - 1 downto 0);
    22.7 -                val P = list_comb (List.nth (preds, i),
    22.8 -                  map (incr_boundvars k) ys @ bs);
    22.9 +                val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs);
   22.10                  val Q = list_abs (mk_names "x" k ~~ Ts,
   22.11                    HOLogic.mk_binop inductive_conj_name
   22.12                      (list_comb (incr_boundvars k s, bs), P))
   22.13 @@ -641,10 +640,11 @@
   22.14          val SOME (_, i, ys, _) = dest_predicate cs params
   22.15            (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
   22.16  
   22.17 -      in list_all_free (Logic.strip_params r,
   22.18 -        Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
   22.19 -          (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
   22.20 -            HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
   22.21 +      in
   22.22 +        list_all_free (Logic.strip_params r,
   22.23 +          Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
   22.24 +            (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
   22.25 +              HOLogic.mk_Trueprop (list_comb (nth preds i, ys))))
   22.26        end;
   22.27  
   22.28      val ind_prems = map mk_ind_prem intr_ts;
    23.1 --- a/src/HOL/Tools/refute.ML	Sat Apr 16 16:37:21 2011 +0200
    23.2 +++ b/src/HOL/Tools/refute.ML	Sat Apr 16 18:11:20 2011 +0200
    23.3 @@ -1628,7 +1628,7 @@
    23.4            Const (_, T) => interpret_groundterm T
    23.5          | Free (_, T) => interpret_groundterm T
    23.6          | Var (_, T) => interpret_groundterm T
    23.7 -        | Bound i => SOME (List.nth (#bounds args, i), model, args)
    23.8 +        | Bound i => SOME (nth (#bounds args) i, model, args)
    23.9          | Abs (x, T, body) =>
   23.10              let
   23.11                (* create all constants of type 'T' *)
   23.12 @@ -2271,7 +2271,7 @@
   23.13                          else ()
   23.14                        (* the type of a recursion operator is *)
   23.15                        (* [T1, ..., Tn, IDT] ---> Tresult     *)
   23.16 -                      val IDT = List.nth (binder_types T, mconstrs_count)
   23.17 +                      val IDT = nth (binder_types T) mconstrs_count
   23.18                        (* by our assumption on the order of recursion operators *)
   23.19                        (* and datatypes, this is the index of the datatype      *)
   23.20                        (* corresponding to the given recursion operator         *)
   23.21 @@ -2463,15 +2463,15 @@
   23.22                                (* find the indices of the constructor's /recursive/ *)
   23.23                                (* arguments                                         *)
   23.24                                val (_, _, constrs) = the (AList.lookup (op =) descr idx)
   23.25 -                              val (_, dtyps)      = List.nth (constrs, c)
   23.26 -                              val rec_dtyps_args  = filter
   23.27 +                              val (_, dtyps) = nth constrs c
   23.28 +                              val rec_dtyps_args = filter
   23.29                                  (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
   23.30                                (* map those indices to interpretations *)
   23.31                                val rec_dtyps_intrs = map (fn (dtyp, arg) =>
   23.32                                  let
   23.33 -                                  val dT     = typ_of_dtyp descr typ_assoc dtyp
   23.34 +                                  val dT = typ_of_dtyp descr typ_assoc dtyp
   23.35                                    val consts = make_constants ctxt (typs, []) dT
   23.36 -                                  val arg_i  = List.nth (consts, arg)
   23.37 +                                  val arg_i = nth consts arg
   23.38                                  in
   23.39                                    (dtyp, arg_i)
   23.40                                  end) rec_dtyps_args
   23.41 @@ -3104,7 +3104,7 @@
   23.42                        (* generate all constants                                 *)
   23.43                        val consts = make_constants ctxt (typs, []) dT
   23.44                      in
   23.45 -                      print ctxt (typs, []) dT (List.nth (consts, n)) assignment
   23.46 +                      print ctxt (typs, []) dT (nth consts n) assignment
   23.47                      end) (cargs ~~ args)
   23.48                  in
   23.49                    SOME (list_comb (cTerm, argsTerms))
    24.1 --- a/src/HOL/Tools/simpdata.ML	Sat Apr 16 16:37:21 2011 +0200
    24.2 +++ b/src/HOL/Tools/simpdata.ML	Sat Apr 16 18:11:20 2011 +0200
    24.3 @@ -59,8 +59,9 @@
    24.4    let
    24.5      fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q
    24.6        | count_imp _ = 0;
    24.7 -    val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
    24.8 -  in if j = 0 then @{thm meta_eq_to_obj_eq}
    24.9 +    val j = count_imp (Logic.strip_assums_concl (nth (prems_of st) (i - 1)))
   24.10 +  in
   24.11 +    if j = 0 then @{thm meta_eq_to_obj_eq}
   24.12      else
   24.13        let
   24.14          val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
   24.15 @@ -69,13 +70,14 @@
   24.16          val aT = TFree ("'a", HOLogic.typeS);
   24.17          val x = Free ("x", aT);
   24.18          val y = Free ("y", aT)
   24.19 -      in Goal.prove_global (Thm.theory_of_thm st) []
   24.20 -        [mk_simp_implies (Logic.mk_equals (x, y))]
   24.21 -        (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
   24.22 -        (fn {prems, ...} => EVERY
   24.23 -         [rewrite_goals_tac @{thms simp_implies_def},
   24.24 -          REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
   24.25 -            map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
   24.26 +      in
   24.27 +        Goal.prove_global (Thm.theory_of_thm st) []
   24.28 +          [mk_simp_implies (Logic.mk_equals (x, y))]
   24.29 +          (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
   24.30 +          (fn {prems, ...} => EVERY
   24.31 +           [rewrite_goals_tac @{thms simp_implies_def},
   24.32 +            REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
   24.33 +              map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
   24.34        end
   24.35    end;
   24.36  
    25.1 --- a/src/HOL/ex/svc_funcs.ML	Sat Apr 16 16:37:21 2011 +0200
    25.2 +++ b/src/HOL/ex/svc_funcs.ML	Sat Apr 16 18:11:20 2011 +0200
    25.3 @@ -137,7 +137,7 @@
    25.4      fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
    25.5        | var (Var((a, 0), T), is) = trans_var (a, T, is)
    25.6        | var (Bound i, is)        =
    25.7 -          let val (a,T) = List.nth (params, i)
    25.8 +          let val (a,T) = nth params i
    25.9            in  trans_var ("B_" ^ a, T, is)  end
   25.10        | var (t $ Bound i, is)    = var(t,i::is)
   25.11              (*removing a parameter from a Var: the bound var index will
    26.1 --- a/src/Provers/blast.ML	Sat Apr 16 16:37:21 2011 +0200
    26.2 +++ b/src/Provers/blast.ML	Sat Apr 16 18:11:20 2011 +0200
    26.3 @@ -1252,7 +1252,7 @@
    26.4    let val thy = Thm.theory_of_thm st0
    26.5        val state = initialize thy
    26.6        val st = Conv.gconv_rule Object_Logic.atomize_prems i st0
    26.7 -      val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
    26.8 +      val skoprem = fromSubgoal thy (nth (prems_of st) (i - 1))
    26.9        val hyps  = strip_imp_prems skoprem
   26.10        and concl = strip_imp_concl skoprem
   26.11        fun cont (tacs,_,choices) =
    27.1 --- a/src/Provers/hypsubst.ML	Sat Apr 16 16:37:21 2011 +0200
    27.2 +++ b/src/Provers/hypsubst.ML	Sat Apr 16 18:11:20 2011 +0200
    27.3 @@ -214,21 +214,24 @@
    27.4  
    27.5  (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
    27.6  fun all_imp_intr_tac hyps i =
    27.7 -  let fun imptac (r, [])    st = reverse_n_tac r i st
    27.8 -        | imptac (r, hyp::hyps) st =
    27.9 -           let val (hyp',_) = List.nth (prems_of st, i-1) |>
   27.10 -                              Logic.strip_assums_concl    |>
   27.11 -                              Data.dest_Trueprop          |> Data.dest_imp
   27.12 -               val (r',tac) = if Pattern.aeconv (hyp,hyp')
   27.13 -                              then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   27.14 -                              else (*leave affected hyps at end*)
   27.15 -                                   (r+1, imp_intr_tac i)
   27.16 -           in
   27.17 -               case Seq.pull(tac st) of
   27.18 -                   NONE       => Seq.single(st)
   27.19 -                 | SOME(st',_) => imptac (r',hyps) st'
   27.20 -           end
   27.21 -  in  imptac (0, rev hyps)  end;
   27.22 +  let
   27.23 +    fun imptac (r, []) st = reverse_n_tac r i st
   27.24 +      | imptac (r, hyp::hyps) st =
   27.25 +          let
   27.26 +            val (hyp', _) =
   27.27 +              nth (prems_of st) (i - 1)
   27.28 +              |> Logic.strip_assums_concl
   27.29 +              |> Data.dest_Trueprop |> Data.dest_imp;
   27.30 +            val (r', tac) =
   27.31 +              if Pattern.aeconv (hyp, hyp')
   27.32 +              then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   27.33 +              else (*leave affected hyps at end*) (r + 1, imp_intr_tac i);
   27.34 +          in
   27.35 +            (case Seq.pull (tac st) of
   27.36 +              NONE => Seq.single st
   27.37 +            | SOME (st', _) => imptac (r', hyps) st')
   27.38 +          end
   27.39 +  in imptac (0, rev hyps) end;
   27.40  
   27.41  
   27.42  fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
    28.1 --- a/src/Provers/order.ML	Sat Apr 16 16:37:21 2011 +0200
    28.2 +++ b/src/Provers/order.ML	Sat Apr 16 18:11:20 2011 +0200
    28.3 @@ -274,8 +274,9 @@
    28.4    (* Internal exception, raised if contradiction ( x < x ) was derived *)
    28.5  
    28.6  fun prove asms =
    28.7 -  let fun pr (Asm i) = List.nth (asms, i)
    28.8 -  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    28.9 +  let
   28.10 +    fun pr (Asm i) = nth asms i
   28.11 +      | pr (Thm (prfs, thm)) = map pr prfs MRS thm;
   28.12    in pr end;
   28.13  
   28.14  (* Internal datatype for inequalities *)
   28.15 @@ -847,16 +848,17 @@
   28.16                 val v = upper edge
   28.17             in
   28.18               if (getIndex u ntc) = xi then
   28.19 -               (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge]
   28.20 -               @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   28.21 -             else (rev_completeComponentPath u)@[edge]
   28.22 -                  @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   28.23 +               completeTermPath x u (nth sccSubgraphs xi) @ [edge] @
   28.24 +               completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
   28.25 +             else
   28.26 +              rev_completeComponentPath u @ [edge] @
   28.27 +                completeTermPath v y' (nth sccSubgraphs (getIndex y' ntc))
   28.28             end
   28.29     in
   28.30 -      if x aconv y then
   28.31 -        [(Le (x, y, (Thm ([], #le_refl less_thms))))]
   28.32 -      else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi))
   28.33 -             else rev_completeComponentPath y )
   28.34 +     if x aconv y then
   28.35 +       [(Le (x, y, (Thm ([], #le_refl less_thms))))]
   28.36 +     else if xi = yi then completeTermPath x y (nth sccSubgraphs xi)
   28.37 +     else rev_completeComponentPath y
   28.38     end;
   28.39  
   28.40  (* ******************************************************************* *)
   28.41 @@ -1016,15 +1018,18 @@
   28.42                  (* if SCC_x is linked to SCC_y via edge e *)
   28.43                   else if ui = xi andalso vi = yi then (
   28.44                     case e of (Less (_, _,_)) => (
   28.45 -                        let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) )
   28.46 -                            val xyLesss = transPath (tl xypath, hd xypath)
   28.47 +                        let
   28.48 +                          val xypath =
   28.49 +                            completeTermPath x u (nth sccSubgraphs ui) @ [e] @
   28.50 +                            completeTermPath v y (nth sccSubgraphs vi)
   28.51 +                          val xyLesss = transPath (tl xypath, hd xypath)
   28.52                          in  (Thm ([getprf xyLesss], #less_imp_neq less_thms)) end)
   28.53                     | _ => (
   28.54                          let
   28.55 -                            val xupath = completeTermPath x u  (List.nth(sccSubgraphs, ui))
   28.56 -                            val uxpath = completeTermPath u x  (List.nth(sccSubgraphs, ui))
   28.57 -                            val vypath = completeTermPath v y  (List.nth(sccSubgraphs, vi))
   28.58 -                            val yvpath = completeTermPath y v  (List.nth(sccSubgraphs, vi))
   28.59 +                            val xupath = completeTermPath x u (nth sccSubgraphs ui)
   28.60 +                            val uxpath = completeTermPath u x (nth sccSubgraphs ui)
   28.61 +                            val vypath = completeTermPath v y (nth sccSubgraphs vi)
   28.62 +                            val yvpath = completeTermPath y v (nth sccSubgraphs vi)
   28.63                              val xuLesss = transPath (tl xupath, hd xupath)
   28.64                              val uxLesss = transPath (tl uxpath, hd uxpath)
   28.65                              val vyLesss = transPath (tl vypath, hd vypath)
   28.66 @@ -1037,15 +1042,18 @@
   28.67                          )
   28.68                    ) else if ui = yi andalso vi = xi then (
   28.69                       case e of (Less (_, _,_)) => (
   28.70 -                        let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
   28.71 -                            val xyLesss = transPath (tl xypath, hd xypath)
   28.72 +                        let
   28.73 +                          val xypath =
   28.74 +                            completeTermPath y u (nth sccSubgraphs ui) @ [e] @
   28.75 +                            completeTermPath v x (nth sccSubgraphs vi)
   28.76 +                          val xyLesss = transPath (tl xypath, hd xypath)
   28.77                          in (Thm ([(Thm ([getprf xyLesss], #less_imp_neq less_thms))] , #not_sym less_thms)) end )
   28.78                       | _ => (
   28.79  
   28.80 -                        let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
   28.81 -                            val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui))
   28.82 -                            val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi))
   28.83 -                            val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi))
   28.84 +                        let val yupath = completeTermPath y u (nth sccSubgraphs ui)
   28.85 +                            val uypath = completeTermPath u y (nth sccSubgraphs ui)
   28.86 +                            val vxpath = completeTermPath v x (nth sccSubgraphs vi)
   28.87 +                            val xvpath = completeTermPath x v (nth sccSubgraphs vi)
   28.88                              val yuLesss = transPath (tl yupath, hd yupath)
   28.89                              val uyLesss = transPath (tl uypath, hd uypath)
   28.90                              val vxLesss = transPath (tl vxpath, hd vxpath)
    29.1 --- a/src/Provers/quasi.ML	Sat Apr 16 16:37:21 2011 +0200
    29.2 +++ b/src/Provers/quasi.ML	Sat Apr 16 18:11:20 2011 +0200
    29.3 @@ -86,8 +86,9 @@
    29.4    (* Internal exception, raised if contradiction ( x < x ) was derived *)
    29.5  
    29.6  fun prove asms =
    29.7 -  let fun pr (Asm i) = List.nth (asms, i)
    29.8 -  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    29.9 +  let
   29.10 +    fun pr (Asm i) = nth asms i
   29.11 +      | pr (Thm (prfs, thm)) = map pr prfs MRS thm;
   29.12    in pr end;
   29.13  
   29.14  (* Internal datatype for inequalities *)
    30.1 --- a/src/Provers/splitter.ML	Sat Apr 16 16:37:21 2011 +0200
    30.2 +++ b/src/Provers/splitter.ML	Sat Apr 16 18:11:20 2011 +0200
    30.3 @@ -157,7 +157,7 @@
    30.4     has a body of type T; otherwise the expansion thm will fail later on
    30.5  *)
    30.6  fun type_test (T, lbnos, apsns) =
    30.7 -  let val (_, U: typ, _) = List.nth (apsns, foldl1 Int.min lbnos)
    30.8 +  let val (_, U: typ, _) = nth apsns (foldl1 Int.min lbnos)
    30.9    in T = U end;
   30.10  
   30.11  (*************************************************************************
   30.12 @@ -270,7 +270,7 @@
   30.13            in snd (fold iter ts (0, a)) end
   30.14    in posns Ts [] [] t end;
   30.15  
   30.16 -fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
   30.17 +fun nth_subgoal i thm = nth (prems_of thm) (i - 1);
   30.18  
   30.19  fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) =
   30.20    prod_ord (int_ord o pairself length) (order o pairself length)
    31.1 --- a/src/Provers/trancl.ML	Sat Apr 16 16:37:21 2011 +0200
    31.2 +++ b/src/Provers/trancl.ML	Sat Apr 16 18:11:20 2011 +0200
    31.3 @@ -95,8 +95,8 @@
    31.4      fun inst thm =
    31.5        let val SOME (_, _, r', _) = decomp (concl_of thm)
    31.6        in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end;
    31.7 -    fun pr (Asm i) = List.nth (asms, i)
    31.8 -      | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm
    31.9 +    fun pr (Asm i) = nth asms i
   31.10 +      | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm;
   31.11    in pr end;
   31.12  
   31.13  
    32.1 --- a/src/Tools/IsaPlanner/rw_tools.ML	Sat Apr 16 16:37:21 2011 +0200
    32.2 +++ b/src/Tools/IsaPlanner/rw_tools.ML	Sat Apr 16 18:11:20 2011 +0200
    32.3 @@ -122,7 +122,7 @@
    32.4  fun fake_concl_of_goal gt i = 
    32.5      let 
    32.6        val prems = Logic.strip_imp_prems gt
    32.7 -      val sgt = List.nth (prems, i - 1)
    32.8 +      val sgt = nth prems (i - 1)
    32.9  
   32.10        val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
   32.11        val tparams = Term.strip_all_vars sgt
   32.12 @@ -140,7 +140,7 @@
   32.13  fun fake_goal gt i = 
   32.14      let 
   32.15        val prems = Logic.strip_imp_prems gt
   32.16 -      val sgt = List.nth (prems, i - 1)
   32.17 +      val sgt = nth prems (i - 1)
   32.18  
   32.19        val tbody = Term.strip_all_body sgt
   32.20        val tparams = Term.strip_all_vars sgt