# HG changeset patch
# User desharna
# Date 1639121974 -3600
# Node ID ece4f07ebb0479e0d4abeaeda68f4fe6e63bdc4b
# Parent  2cbb5f6a854f98a94b18c36f4d1e5fd7ebed4a14
fixed HOL-TPTP

diff -r 2cbb5f6a854f -r ece4f07ebb04 src/HOL/TPTP/ATP_Theory_Export.thy
--- 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>
diff -r 2cbb5f6a854f -r ece4f07ebb04 src/HOL/TPTP/atp_problem_import.ML
--- 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\")"))
diff -r 2cbb5f6a854f -r ece4f07ebb04 src/HOL/TPTP/atp_theory_export.ML
--- 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? *)