# HG changeset patch
# User boehmes
# Date 1292499186 -3600
# Node ID d23af676f9f8097a2ac483e3c4d4dfe0553dd25f
# Parent  f59491d5632715f5bc35121902bba74b4f6b6dcb
fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term

diff -r f59491d56327 -r d23af676f9f8 src/HOL/Tools/SMT/smt_translate.ML
--- 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)