1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:12:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:21:19 2011 +0200
     1.3 @@ -532,15 +532,16 @@
     1.4             if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
     1.5           else if trans = lambdasN andalso
     1.6                   not (is_type_enc_higher_order type_enc) then
     1.7 -           error ("Lambda translation method incompatible with \
     1.8 -                  \first-order encoding.")
     1.9 +           error ("Lambda translation method incompatible with first-order \
    1.10 +                  \encoding.")
    1.11           else
    1.12             trans)
    1.13    |> (fn trans =>
    1.14           if trans = concealedN then
    1.15             rpair [] o map (conceal_lambdas ctxt)
    1.16           else if trans = liftingN then
    1.17 -           SMT_Translate.lift_lambdas ctxt false #> snd #> swap
    1.18 +           map (close_form o Envir.eta_contract)
    1.19 +           #> SMT_Translate.lift_lambdas ctxt false #> snd #> swap
    1.20           else if trans = combinatorsN then
    1.21             rpair [] o map (introduce_combinators ctxt)
    1.22           else if trans = lambdasN then