--- 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)
--- 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