--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jan 30 17:15:59 2012 +0100
@@ -1705,9 +1705,11 @@
lift_lams_part_1 ctxt type_enc
##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
#> lift_lams_part_2
- else if lam_trans = combs_or_liftingN then (* ### FIXME: implement *)
+ else if lam_trans = combs_or_liftingN then
lift_lams_part_1 ctxt type_enc
- ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
+ ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
+ @{term "op =::bool => bool => bool"} => t
+ | _ => introduce_combinators ctxt (intentionalize_def t))
#> lift_lams_part_2
else if lam_trans = keep_lamsN then
map (Envir.eta_contract) #> rpair []