fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term

--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:07:36 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:33:06 2010 +0100
@@ -361,7 +361,7 @@
       | (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)