# HG changeset patch # User desharna # Date 1627410503 -7200 # Node ID 2af4e088c01c4c90fcb6297a859d248c77e3bf29 # Parent 6c8473b4f51862fff13934e9249529471065e42d# Parent dc98bb7a439bf45b9849030d62e7ab1f8aa1582f merged diff -r dc98bb7a439b -r 2af4e088c01c src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 27 15:31:54 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 27 20:28:23 2021 +0200 @@ -2084,7 +2084,7 @@ | IVar (name, _) => map (term Elsewhere) args |> mk_aterm type_enc name [] | IAbs ((name, T), tm) => - if is_type_enc_higher_order type_enc then + if is_type_enc_higher_order type_enc orelse is_type_enc_fool type_enc then AAbs (((name, native_atp_type_of_typ type_enc false 0 T), term Elsewhere tm), map (term Elsewhere) args) else