# HG changeset patch
# User desharna
# Date 1605195742 -3600
# Node ID 56514a42eee836117d8461ba8b9355eb272f587b
# Parent  7b7227d9ae5e5024ec2d69ecd8c00803808b02d6
Updated ML in forgotten in previous commit

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