# HG changeset patch
# User blanchet
# Date 1648212743 -3600
# Node ID 62f0fda48a39d9e41f3536770860261e8d222632
# Parent  959a74c665d2c1932bea3b1a328a6f56fcbfeb2b
compile mirabelle

diff -r 959a74c665d2 -r 62f0fda48a39 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Mar 25 13:52:23 2022 +0100
@@ -23,7 +23,6 @@
 val keep_probsK = "keep_probs" (*=BOOL: keep temporary problem files created by sledgehammer*)
 val keep_proofsK = "keep_proofs" (*=BOOL: keep temporary proof files created by ATPs*)
 val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*)
-val term_orderK = "term_order" (*=STRING: term order (in E)*)
 
 (*defaults used in this Mirabelle action*)
 val check_trivial_default = false
@@ -271,7 +270,7 @@
 
 local
 
-fun run_sh params term_order keep pos state =
+fun run_sh params keep pos state =
   let
     fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
         let
@@ -285,12 +284,8 @@
           #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
         end
       | set_file_name NONE = I
-    val state' =
-      state
-      |> Proof.map_context
-           (set_file_name keep
-            #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order)
-                  term_order |> the_default I))
+    val state' = state
+      |> Proof.map_context (set_file_name keep)
 
     val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
       Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
@@ -304,8 +299,8 @@
 
 in
 
-fun run_sledgehammer (params as {provers, ...}) output_dir term_order
-  keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st =
+fun run_sledgehammer (params as {provers, ...}) output_dir keep_probs keep_proofs
+    proof_method_from_msg thy_index trivial pos st =
   let
     val thy = Proof.theory_of st
     val thy_name = Context.theory_name thy
@@ -321,7 +316,7 @@
       else
         NONE
     val prover_name = hd provers
-    val (sledgehamer_outcome, msg, cpu_time) = run_sh params term_order keep pos st
+    val (sledgehamer_outcome, msg, cpu_time) = run_sh params keep pos st
     val (time_prover, change_data, proof_method_and_used_thms) =
       (case sledgehamer_outcome of
         Sledgehammer.SH_Some {used_facts, run_time, ...} =>
@@ -439,7 +434,6 @@
       Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default)
     val keep_probs = Mirabelle.get_bool_argument arguments (keep_probsK, keep_probs_default)
     val keep_proofs = Mirabelle.get_bool_argument arguments (keep_proofsK, keep_proofs_default)
-    val term_order = AList.lookup (op =) arguments term_orderK
     val proof_method_from_msg = proof_method_from_msg arguments
 
     val params = Sledgehammer_Commands.default_params \<^theory> arguments
@@ -456,8 +450,8 @@
           let
             val trivial = check_trivial andalso try0 pre handle Timeout.TIMEOUT _ => false
             val (outcome, log1, change_data1, proof_method_and_used_thms) =
-              run_sledgehammer params output_dir term_order keep_probs keep_proofs
-                proof_method_from_msg theory_index trivial pos pre
+              run_sledgehammer params output_dir keep_probs keep_proofs proof_method_from_msg
+                theory_index trivial pos pre
             val (log2, change_data2) =
               (case proof_method_and_used_thms of
                 SOME (proof_method, used_thms) =>