fixed eta-expansion: use correct order to apply new bound variables
authorboehmes
Fri Apr 08 19:04:08 2011 +0200 (2011-04-08)
changeset 42321ce83c1654b86
parent 42320 1f09e4c680fc
child 42322 be1c32069daa
fixed eta-expansion: use correct order to apply new bound variables
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Apr 08 19:04:08 2011 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Apr 08 19:04:08 2011 +0200
     1.3 @@ -471,6 +471,8 @@
     1.4  
     1.5  lemma True using let_rsp by smt
     1.6  
     1.7 +lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt
     1.8 +
     1.9  lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps)
    1.10  
    1.11  
     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
     2.3 @@ -184,7 +184,7 @@
     2.4      let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
     2.5      in
     2.6        Term.incr_boundvars (length Ts) t
     2.7 -      |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
     2.8 +      |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1)
     2.9        |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
    2.10      end
    2.11  in