--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 20 09:23:12 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 20 12:23:20 2011 +0200
@@ -540,8 +540,9 @@
if trans = concealedN then
rpair [] o map (conceal_lambdas ctxt)
else if trans = liftingN then
- map (close_form o Envir.eta_contract)
- #> Lambda_Lifting.lift_lambdas ctxt false #> snd #> swap
+ map (close_form o Envir.eta_contract) #> rpair ctxt
+ #-> Lambda_Lifting.lift_lambdas NONE Lambda_Lifting.is_quantifier
+ #> fst
else if trans = combinatorsN then
rpair [] o map (introduce_combinators ctxt)
else if trans = lambdasN then