--- 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
--- 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)) =
--- 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", _)] =
--- 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
--- 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)
--- 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) =
--- 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) =
--- 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