diff -r 77435a7853d1 -r c3979dd80a50 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Nov 25 14:13:48 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Nov 25 14:58:20 2010 +0100
@@ -402,6 +402,9 @@
               | NONE => transs h T ts))
       | (h as Free (_, T), ts) => transs h T ts
       | (Bound i, []) => pair (SVar i)
+      | (Abs (_, _, t1 $ Bound 0), []) =>
+        if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *)
+        else raise TERM ("smt_translate", [t])
       | _ => raise TERM ("smt_translate", [t]))
 
     and transs t T ts =