--- 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>
--- a/src/HOL/TPTP/atp_problem_import.ML Thu Dec 09 14:20:55 2021 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Dec 10 08:39:34 2021 +0100
@@ -246,8 +246,6 @@
ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac lthy i)
-fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
-
fun make_conj (defs, nondefs) conjs =
Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => \<^prop>\<open>False\<close>)
@@ -298,9 +296,9 @@
val (format, type_enc, lam_trans) =
(case format_str of
"FOF" => (FOF, "mono_guards??", liftingN)
- | "TF0" => (TFF (Without_FOOL, Monomorphic), "mono_native", liftingN)
- | "TH0" => (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher",
- keep_lamsN)
+ | "TF0" => (TFF (Monomorphic, Without_FOOL), "mono_native", liftingN)
+ | "TH0" => (THF (Monomorphic, {with_ite = false, with_let = false}, 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 Dec 09 14:20:55 2021 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Dec 10 08:39:34 2021 +0100
@@ -36,11 +36,11 @@
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 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? *)