--- 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>
--- a/src/HOL/TPTP/atp_problem_import.ML Thu Nov 12 16:18:43 2020 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Thu Nov 12 16:42:22 2020 +0100
@@ -298,8 +298,9 @@
val (format, type_enc, lam_trans) =
(case format_str of
"FOF" => (FOF, "mono_guards??", liftingN)
- | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
- | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+ | "TF0" => (TFF (Without_FOOL, Monomorphic), "mono_native", liftingN)
+ | "TH0" => (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher",
+ keep_lamsN)
| "DFG" => (DFG Monomorphic, "mono_native", liftingN)
| _ => error ("Unknown format " ^ quote format_str ^
" (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
--- a/src/HOL/TPTP/atp_theory_export.ML Thu Nov 12 16:18:43 2020 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Nov 12 16:42:22 2020 +0100
@@ -36,12 +36,12 @@
val prefix = Library.prefix
val fact_name_of = prefix fact_prefix o ascii_of
-fun atp_of_format (THF (Polymorphic, _)) = leo3N
- | atp_of_format (THF (Monomorphic, _)) = satallaxN
+fun atp_of_format (THF (_, Polymorphic, _)) = leo3N
+ | atp_of_format (THF (_, Monomorphic, _)) = satallaxN
| atp_of_format (DFG Polymorphic) = pirateN
| atp_of_format (DFG Monomorphic) = spassN
- | atp_of_format (TFF Polymorphic) = alt_ergoN
- | atp_of_format (TFF Monomorphic) = vampireN
+ | atp_of_format (TFF (_, Polymorphic)) = alt_ergoN
+ | atp_of_format (TFF (_, Monomorphic)) = vampireN
| atp_of_format FOF = eN (* FIXME? *)
| atp_of_format CNF_UEQ = waldmeisterN
| atp_of_format CNF = eN (* FIXME? *)