src/HOL/Tools/SMT/smt_translate.ML

         (u as Const (_, T), ts) => apply terms T u (map (traverse env) ts)
       | (u as Free (_, T), ts) => apply terms T u (map (traverse env) ts)
       | (u as Bound i, ts) =>
           appl0 (nth arities i) (map (traverse env) ts) (u, nth Ts i)
       | (Abs (n, T, u), ts) =>
-          let val env' = (get_arities 0 u [] :: arities, T :: Ts)
+          let val env' = (get_arities 0 u [0] :: arities, T :: Ts)
           in traverses env (Abs (n, T, traverse env' u)) ts end
       | (u, ts) => traverses env u ts)
     and traverses env t ts = Term.list_comb (t, map (traverse env) ts)
   in map (traverse ([], [])) ts end