src/HOL/TPTP/ATP_Theory_Export.thy
changeset 72591 56514a42eee8
parent 69605 a96320074298
child 74902 ece4f07ebb04
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Thu Nov 12 16:18:43 2020 +0100
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Thu Nov 12 16:42:22 2020 +0100
@@ -25,8 +25,8 @@
 ML \<open>
 if do_it then
   "/tmp/isa_filter"
-  |> generate_casc_lbt_isa_files_for_theory ctxt thy (THF (Polymorphic, THF_Without_Choice))
-         infer_policy "poly_native_higher"
+  |> generate_casc_lbt_isa_files_for_theory ctxt thy
+      (THF (Without_FOOL, Polymorphic, THF_Without_Choice)) infer_policy "poly_native_higher"
 else
   ()
 \<close>