diff -r 8b1ab558e3ee -r e83224066f19 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun Nov 28 14:15:01 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun Nov 28 21:16:35 2021 +0100
@@ -277,7 +277,7 @@
     fun make_builtin arity is_predicate name = (name, {arity = arity, is_predicate = is_predicate})
   in
     map (make_builtin 0 true) [tptp_false, tptp_true] @
-    map (make_builtin 1 true) [tptp_not] @
+    map (make_builtin 1 true) [tptp_not, tptp_ho_forall, tptp_ho_exists] @
     map (make_builtin 2 true) [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
       tptp_equal, tptp_old_equal] @
     map (make_builtin 2 false) [tptp_let] @