# HG changeset patch
# User blanchet
# Date 1648212743 -3600
# Node ID 647611e6da76d29e53014c03dd8b9f6471532011
# Parent  62f0fda48a39d9e41f3536770860261e8d222632
compile TPTP module

diff -r 62f0fda48a39 -r 647611e6da76 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -313,9 +313,7 @@
         Translator
         lam_trans uncurried_aliases readable_names presimp [] conj facts
 
-    val ord = Sledgehammer_ATP_Systems.effective_term_order lthy spassN
-    val ord_info = K []
-    val lines = lines_of_atp_problem format ord ord_info atp_problem
+    val lines = lines_of_atp_problem format (K []) atp_problem
   in
     List.app Output.physical_stdout lines
   end
diff -r 62f0fda48a39 -r 647611e6da76 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -51,14 +51,13 @@
     val prob_file = File.tmp_path (Path.explode "prob")
     val atp = atp_of_format format
     val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp ()
-    val ord = effective_term_order ctxt atp
     val _ = problem
-      |> lines_of_atp_problem format ord (K [])
+      |> lines_of_atp_problem format (K [])
       |> File.write_list prob_file
     val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
     val command =
       space_implode " " (File.bash_path (Path.explode path) ::
-        arguments ctxt false "" atp_timeout prob_file (ord, K [], K []))
+        arguments ctxt false "" atp_timeout prob_file)
     val outcome =
       Timeout.apply atp_timeout Isabelle_System.bash_output command
       |> fst
@@ -208,9 +207,6 @@
      |> order_problem_facts name_ord)
   end
 
-fun lines_of_problem ctxt format =
-  lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K [])
-
 fun write_lines path ss =
   let
     val _ = File.write path ""
@@ -220,7 +216,7 @@
 fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc file_name =
   let
     val (_, problem) = problem_of_theory ctxt thy format infer_policy type_enc
-    val ss = lines_of_problem ctxt format problem
+    val ss = lines_of_atp_problem format (K []) problem
   in write_lines (Path.explode file_name) ss end
 
 fun ap dir = Path.append dir o Path.explode
@@ -302,7 +298,7 @@
     val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts)
 
     fun write_prelude () =
-      let val ss = lines_of_problem ctxt format prelude in
+      let val ss = lines_of_atp_problem format (K []) prelude in
         File.append file_order_path (prelude_base_name ^ "\n");
         write_lines (ap include_dir prelude_name) ss
       end
@@ -310,7 +306,7 @@
     fun write_include_file (base_name, fact_lines) =
       let
         val name = base_name ^ include_suffix
-        val ss = lines_of_problem ctxt format [(factsN, fact_lines)]
+        val ss = lines_of_atp_problem format (K []) [(factsN, fact_lines)]
       in
         File.append file_order_path (base_name ^ "\n");
         write_lines (ap include_dir name) ss