src/Pure/proofterm.ML

 fun prf_subst_bounds args prf =
   let
     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)
       | subst' _ _ = raise SAME
     and substh' lev t = (subst' lev t handle SAME => t);

 fun prf_subst_pbounds args prf =
   let
     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))
       | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev
           handle SAME => prf %% subst prf' Plev tlev)

       | shrink' ls lev ts prfs (prf as prf1 % t) =
           let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
           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)
       | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp t)
       | shrink' ls lev ts prfs MinProof = ([], false, map (pair false) ts, MinProof)