Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
really keep lambdas in translation if only predicates are missing
authorblanchet
Tue, 22 Jan 2019 17:57:19 +0100
changeset 69718 f7f3ed2eea0a
parent 69717 eb74ff534b27
child 69719 331ef175a112
really keep lambdas in translation if only predicates are missing
src/HOL/Tools/ATP/atp_problem_generate.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle