src/HOL/Tools/SMT/smt_translate.ML
changeset 41195 f59491d56327
parent 41173 7c6178d45cc8
child 41196 d23af676f9f8
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 11:31:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:07:36 2010 +0100
     1.3 @@ -202,7 +202,12 @@
     1.4  
     1.5    fun expf t i T ts =
     1.6      let val Ts = U.dest_funT i T |> fst |> drop (length ts)
     1.7 -    in Term.list_comb (t, ts) |> fold_rev eta Ts end
     1.8 +    in
     1.9 +      Term.list_comb (t, ts)
    1.10 +      |> Term.incr_boundvars (length Ts)
    1.11 +      |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
    1.12 +      |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
    1.13 +    end
    1.14  
    1.15    fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
    1.16      | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t