src/HOL/Proofs/Lambda/WeakNorm.thy

         | _ => error "term_of_dB: function type expected"
       end
   | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
 
 fun typing_of_term Ts e (Bound i) =
-      Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i)))
+      Norm.Var (e, nat_of_int i, dBtype_of_typ (nth Ts i))
   | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
         Type ("fun", [T, U]) => Norm.rtypingT_App (e, dB_of_term t,
           dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
           typing_of_term Ts e t, typing_of_term Ts e u)
       | _ => error "typing_of_term: function type expected")