# HG changeset patch
# User wenzelm
# Date 1235749132 -3600
# Node ID a77fc0209723f0352408a3ed200b2c515703bfff
# Parent  09817540ccae17d9effa6f8ae2302ae3e9ae637e
eliminated NJ's List.nth;

diff -r 09817540ccae -r a77fc0209723 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Fri Feb 27 16:33:11 2009 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Fri Feb 27 16:38:52 2009 +0100
@@ -56,7 +56,7 @@
       | thm_of _ _ (PAxm (name, _, SOME Ts)) =
           thm_of_atom (Thm.axiom thy name) Ts
 
-      | thm_of _ Hs (PBound i) = List.nth (Hs, i)
+      | thm_of _ Hs (PBound i) = nth Hs i
 
       | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
           let
diff -r 09817540ccae -r a77fc0209723 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Fri Feb 27 16:33:11 2009 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Fri Feb 27 16:38:52 2009 +0100
@@ -98,7 +98,7 @@
           let val (env3, V) = mk_tvar (env2, [])
           in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
       end
-  | infer_type thy env Ts vTs (t as Bound i) = ((t, List.nth (Ts, i), vTs, env)
+  | infer_type thy env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
       handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
 
 fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^
@@ -152,7 +152,7 @@
     fun head_norm (prop, prf, cnstrts, env, vTs) =
       (Envir.head_norm env prop, prf, cnstrts, env, vTs);
 
-    fun mk_cnstrts env _ Hs vTs (PBound i) = ((List.nth (Hs, i), PBound i, [], env, vTs)
+    fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs)
           handle Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i))
       | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
           let
@@ -304,7 +304,7 @@
 
 val head_norm = Envir.head_norm (Envir.empty 0);
 
-fun prop_of0 Hs (PBound i) = List.nth (Hs, i)
+fun prop_of0 Hs (PBound i) = nth Hs i
   | prop_of0 Hs (Abst (s, SOME T, prf)) =
       Term.all T $ (Abs (s, T, prop_of0 Hs prf))
   | prop_of0 Hs (AbsP (s, SOME t, prf)) =
diff -r 09817540ccae -r a77fc0209723 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri Feb 27 16:33:11 2009 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Fri Feb 27 16:38:52 2009 +0100
@@ -222,7 +222,7 @@
 (* implicit structures *)
 
 fun the_struct structs i =
-  if 1 <= i andalso i <= length structs then List.nth (structs, i - 1)
+  if 1 <= i andalso i <= length structs then nth structs (i - 1)
   else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
 
 fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
diff -r 09817540ccae -r a77fc0209723 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Feb 27 16:33:11 2009 +0100
+++ b/src/Pure/envir.ML	Fri Feb 27 16:38:52 2009 +0100
@@ -265,7 +265,7 @@
       | fast Ts (Const (_, T)) = T
       | fast Ts (Free (_, T)) = T
       | fast Ts (Bound i) =
-        (List.nth (Ts, i)
+        (nth Ts i
          handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
       | fast Ts (Var (_, T)) = T
       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
diff -r 09817540ccae -r a77fc0209723 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Feb 27 16:33:11 2009 +0100
+++ b/src/Pure/proofterm.ML	Fri Feb 27 16:38:52 2009 +0100
@@ -470,8 +470,8 @@
     val n = length args;
     fun subst' lev (Bound i) =
          (if i<lev then raise SAME    (*var is locally bound*)
-          else  incr_boundvars lev (List.nth (args, i-lev))
-                  handle Subscript => Bound (i-n)  (*loose: change it*))
+          else  incr_boundvars lev (nth args (i-lev))
+                  handle Subscript => Bound (i-n))  (*loose: change it*)
       | subst' lev (Abs (a, T, body)) = Abs (a, T,  subst' (lev+1) body)
       | subst' lev (f $ t) = (subst' lev f $ substh' lev t
           handle SAME => f $ subst' lev t)
@@ -494,7 +494,7 @@
     val n = length args;
     fun subst (PBound i) Plev tlev =
          (if i < Plev then raise SAME    (*var is locally bound*)
-          else incr_pboundvars Plev tlev (List.nth (args, i-Plev))
+          else incr_pboundvars Plev tlev (nth args (i-Plev))
                  handle Subscript => PBound (i-n)  (*loose: change it*))
       | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
       | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
@@ -935,7 +935,7 @@
           in (is, ch orelse ch', ts',
               if ch orelse ch' then prf' % t' else prf) end
       | shrink' ls lev ts prfs (prf as PBound i) =
-          (if exists (fn SOME (Bound j) => lev-j <= List.nth (ls, i) | _ => true) ts
+          (if exists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts
              orelse has_duplicates (op =)
                (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
              orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
diff -r 09817540ccae -r a77fc0209723 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Feb 27 16:33:11 2009 +0100
+++ b/src/Pure/sign.ML	Fri Feb 27 16:38:52 2009 +0100
@@ -338,7 +338,7 @@
     fun typ_of (_, Const (_, T)) = T
       | typ_of (_, Free  (_, T)) = T
       | typ_of (_, Var (_, T)) = T
-      | typ_of (bs, Bound i) = snd (List.nth (bs, i) handle Subscript =>
+      | typ_of (bs, Bound i) = snd (nth bs i handle Subscript =>
           raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
       | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
       | typ_of (bs, t $ u) =
diff -r 09817540ccae -r a77fc0209723 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Feb 27 16:33:11 2009 +0100
+++ b/src/Pure/term.ML	Fri Feb 27 16:38:52 2009 +0100
@@ -297,7 +297,7 @@
   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
 fun type_of1 (Ts, Const (_,T)) = T
   | type_of1 (Ts, Free  (_,T)) = T
-  | type_of1 (Ts, Bound i) = (List.nth (Ts,i)
+  | type_of1 (Ts, Bound i) = (nth Ts i
         handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   | type_of1 (Ts, Var (_,T)) = T
   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
@@ -322,7 +322,7 @@
         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   | fastype_of1 (_, Const (_,T)) = T
   | fastype_of1 (_, Free (_,T)) = T
-  | fastype_of1 (Ts, Bound i) = (List.nth(Ts,i)
+  | fastype_of1 (Ts, Bound i) = (nth Ts i
          handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
   | fastype_of1 (_, Var (_,T)) = T
   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
@@ -638,7 +638,7 @@
     val n = length args;
     fun subst (t as Bound i, lev) =
          (if i < lev then raise SAME   (*var is locally bound*)
-          else incr_boundvars lev (List.nth (args, i - lev))
+          else incr_boundvars lev (nth args (i - lev))
             handle Subscript => Bound (i - n))  (*loose: change it*)
       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
       | subst (f $ t, lev) =
diff -r 09817540ccae -r a77fc0209723 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Feb 27 16:33:11 2009 +0100
+++ b/src/Pure/type_infer.ML	Fri Feb 27 16:38:52 2009 +0100
@@ -369,7 +369,7 @@
     fun inf _ (PConst (_, T)) = T
       | inf _ (PFree (_, T)) = T
       | inf _ (PVar (_, T)) = T
-      | inf bs (PBound i) = snd (List.nth (bs, i) handle Subscript => err_loose i)
+      | inf bs (PBound i) = snd (nth bs i handle Subscript => err_loose i)
       | inf bs (PAbs (x, T, t)) = PType ("fun", [T, inf ((x, T) :: bs) t])
       | inf bs (PAppl (t, u)) =
           let