src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML

    val .*K = "PARAMETER" (*DESCRIPTION*)
 *)
 (* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *)
 
 val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*)
-val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*)
 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)*)
 

     else
       "smt")
 
 local
 
-fun run_sh params e_selection_heuristic term_order keep pos state =
+fun run_sh params term_order keep pos state =
   let
     fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
         let
           val filename = "prob_" ^
             StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^

       | set_file_name NONE = I
     val state' =
       state
       |> Proof.map_context
            (set_file_name keep
-            #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic)
-                  e_selection_heuristic |> the_default I)
             #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order)
                   term_order |> the_default I))
 
     val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
       Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1

     ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0)
   | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
 
 in
 
-fun run_sledgehammer (params as {provers, ...}) output_dir e_selection_heuristic term_order
+fun run_sledgehammer (params as {provers, ...}) output_dir term_order
   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
     val triv_str = if trivial then "[T] " else ""

           |> (fn dir => SOME (dir, keep_probs, keep_proofs))
         end
       else
         NONE
     val prover_name = hd provers
-    val (sledgehamer_outcome, msg, cpu_time) =
-      run_sh params e_selection_heuristic term_order keep pos st
+    val (sledgehamer_outcome, msg, cpu_time) = run_sh params term_order keep pos st
     val (time_prover, change_data, proof_method_and_used_thms) =
       (case sledgehamer_outcome of
         Sledgehammer.SH_Some {used_facts, run_time, ...} =>
         let
           val num_used_facts = length used_facts

     (* Parse Mirabelle-specific parameters *)
     val check_trivial =
       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 e_selection_heuristic = AList.lookup (op =) arguments e_selection_heuristicK
     val term_order = AList.lookup (op =) arguments term_orderK
     val proof_method_from_msg = proof_method_from_msg arguments
 
     (* Parse Sledgehammer parameters *)
     val params = Sledgehammer_Commands.default_params \<^theory> arguments

           ""
         else
           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 e_selection_heuristic term_order
-                keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre
+              run_sledgehammer params output_dir term_order 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) =>
                 run_proof_method trivial false name proof_method used_thms timeout pos pre
                 |> apfst (prefix (proof_method ^ " (sledgehammer): "))