really keep lambdas in translation if only predicates are missing
authorblanchet
Tue Jan 22 17:57:19 2019 +0100 (5 months ago ago)
changeset 69734f7f3ed2eea0a
parent 69733 eb74ff534b27
child 69735 331ef175a112
really keep lambdas in translation if only predicates are missing
src/HOL/Tools/ATP/atp_problem_generate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 22 17:22:09 2019 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 22 17:57:19 2019 +0100
     1.3 @@ -2614,7 +2614,7 @@
     1.4        else
     1.5          Sufficient_App_Op_And_Predicator
     1.6      val lam_trans =
     1.7 -      if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN
     1.8 +      if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN
     1.9        else lam_trans
    1.10      val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) =
    1.11        translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts