# HG changeset patch
# User desharna
# Date 1627410342 -7200
# Node ID 6c8473b4f51862fff13934e9249529471065e42d
# Parent  ffbd1b7e54397f551fc71143347758aaef9a552a
fixed TFX generation when universal quantifier is used as term

diff -r ffbd1b7e5439 -r 6c8473b4f518 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jul 27 13:39:18 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jul 27 20:25:42 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