# HG changeset patch
# User boehmes
# Date 1302282248 -7200
# Node ID ce83c1654b86d7ec52d5e5f5fda13ba70f581476
# Parent  1f09e4c680fc6e24ab45d85dbbc073470f01ad15
fixed eta-expansion: use correct order to apply new bound variables

diff -r 1f09e4c680fc -r ce83c1654b86 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Apr 08 19:04:08 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Apr 08 19:04:08 2011 +0200
@@ -471,6 +471,8 @@
 
 lemma True using let_rsp by smt
 
+lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt
+
 lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps)
 
 
diff -r 1f09e4c680fc -r ce83c1654b86 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
@@ -184,7 +184,7 @@
     let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
     in
       Term.incr_boundvars (length Ts) t
-      |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
+      |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1)
       |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
     end
 in