# HG changeset patch
# User blanchet
# Date 1327940159 -3600
# Node ID ded0390eceae59f78c8c0acd4b796f99a0c5f308
# Parent  723343a03abeae770766c7e5bd07e219d23a2ef2
implemented new lambda translations scheme

diff -r 723343a03abe -r ded0390eceae src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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 []