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>