# HG changeset patch
# User blanchet
# Date 1548176239 -3600
# Node ID f7f3ed2eea0a9abb388ee9b147cf9a98d6bde80d
# Parent  eb74ff534b27c2471219595f9cc0806e2f3f3e53
really keep lambdas in translation if only predicates are missing

diff -r eb74ff534b27 -r f7f3ed2eea0a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 22 17:22:09 2019 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 22 17:57:19 2019 +0100
@@ -2614,7 +2614,7 @@
       else
         Sufficient_App_Op_And_Predicator
     val lam_trans =
-      if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
+      if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
       else lam_trans
     val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
       translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts