# HG changeset patch
# User blanchet
# Date 1290693500 -3600
# Node ID c3979dd80a50c192aff0dbf1d33de01594ff0c76
# Parent  77435a7853d1bfa3457406f57e71e320e743dbd4
eta-reduce on the fly to prevent an exception

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 =