--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Thu Dec 09 14:20:55 2021 +0100
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Fri Dec 10 08:39:34 2021 +0100
@@ -26,7 +26,8 @@
 if do_it then
   "/tmp/isa_filter"
   |> generate_casc_lbt_isa_files_for_theory ctxt thy
-      (THF (Without_FOOL, Polymorphic, THF_Without_Choice)) infer_policy "poly_native_higher"
+     (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice)) infer_policy
+     "poly_native_higher"
 else
   ()
 \<close>