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.
merged
authordesharna
Tue, 27 Jul 2021 20:28:23 +0200
changeset 74074 2af4e088c01c
parent 74073 6c8473b4f518 (diff)
parent 74072 dc98bb7a439b (current diff)
child 74075 a5bab59d580b
merged
--- 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
isabelle