--- 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)) =