src/HOL/Tools/SMT/smt_translate.ML
changeset 41196 d23af676f9f8
parent 41195 f59491d56327
child 41197 edab1efe0a70
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:07:36 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:33:06 2010 +0100
     1.3 @@ -361,7 +361,7 @@
     1.4        | (u as Bound i, ts) =>
     1.5            appl0 (nth arities i) (map (traverse env) ts) (u, nth Ts i)
     1.6        | (Abs (n, T, u), ts) =>
     1.7 -          let val env' = (get_arities 0 u [] :: arities, T :: Ts)
     1.8 +          let val env' = (get_arities 0 u [0] :: arities, T :: Ts)
     1.9            in traverses env (Abs (n, T, traverse env' u)) ts end
    1.10        | (u, ts) => traverses env u ts)
    1.11      and traverses env t ts = Term.list_comb (t, map (traverse env) ts)