# HG changeset patch
# User boehmes
# Date 1292497656 -3600
# Node ID f59491d5632715f5bc35121902bba74b4f6b6dcb
# Parent  8aace46ffecb3828bf544641cf317b9a999b90dc
fixed eta-expansion: introduce a couple of abstractions at once

diff -r 8aace46ffecb -r f59491d56327 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 11:31:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:07:36 2010 +0100
@@ -202,7 +202,12 @@
 
   fun expf t i T ts =
     let val Ts = U.dest_funT i T |> fst |> drop (length ts)
-    in Term.list_comb (t, ts) |> fold_rev eta Ts end
+    in
+      Term.list_comb (t, ts)
+      |> Term.incr_boundvars (length Ts)
+      |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
+      |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
+    end
 
   fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
     | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t