removed obscure E option

--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -20,7 +20,6 @@
 (* 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)*)
@@ -272,7 +271,7 @@
 
 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
@@ -290,8 +289,6 @@
       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))
 
@@ -307,7 +304,7 @@
 
 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
@@ -324,8 +321,7 @@
       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, ...} =>
@@ -444,7 +440,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 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
 
@@ -467,8 +462,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 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) =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -32,7 +32,6 @@
   val e_autoN : string
   val e_fun_weightN : string
   val e_sym_offset_weightN : string
-  val e_selection_heuristic : string Config.T
   val e_default_fun_weight : real Config.T
   val e_fun_weight_base : real Config.T
   val e_fun_weight_span : real Config.T
@@ -208,8 +207,6 @@
 val e_fun_weightN = "fun_weight"
 val e_sym_offset_weightN = "sym_offset_weight"
 
-val e_selection_heuristic =
-  Attrib.setup_config_string \<^binding>\<open>atp_e_selection_heuristic\<close> (K e_smartN)
 (* FUDGE *)
 val e_default_fun_weight =
   Attrib.setup_config_real \<^binding>\<open>atp_e_default_fun_weight\<close> (K 20.0)
@@ -291,7 +288,6 @@
    prem_role = Conjecture,
    good_slices = fn ctxt =>
      let
-       val heuristic = Config.get ctxt e_selection_heuristic
        val (format, enc, main_lam_trans) =
          if string_ord (getenv "E_VERSION", "2.7") <> LESS then
            (THF (Monomorphic, {with_ite = true, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN)
@@ -301,15 +297,12 @@
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN)
      in
        (* FUDGE *)
-       if heuristic = e_smartN then
-         [((128, meshN), (format, enc, main_lam_trans, false, e_fun_weightN)),
-          ((128, mashN), (format, enc, main_lam_trans, false, e_sym_offset_weightN)),
-          ((91, mepoN), (format, enc, main_lam_trans, false, e_autoN)),
-          ((1000, meshN), (format, "poly_guards??", main_lam_trans, false, e_sym_offset_weightN)),
-          ((256, mepoN), (format, enc, liftingN, false, e_fun_weightN)),
-          ((64, mashN), (format, enc, combsN, false, e_fun_weightN))]
-       else
-         [((500, meshN), (format, enc, combsN, false, heuristic))]
+       [((128, meshN), (format, enc, main_lam_trans, false, e_fun_weightN)),
+        ((128, mashN), (format, enc, main_lam_trans, false, e_sym_offset_weightN)),
+        ((91, mepoN), (format, enc, main_lam_trans, false, e_autoN)),
+        ((1000, meshN), (format, "poly_guards??", main_lam_trans, false, e_sym_offset_weightN)),
+        ((256, mepoN), (format, enc, liftingN, false, e_fun_weightN)),
+        ((64, mashN), (format, enc, combsN, false, e_fun_weightN))]
      end,
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = default_max_new_mono_instances}