src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

                   e_selection_heuristic |> the_default I)
             #> (Option.map (Config.put ATP_Systems.term_order)
                   term_order |> the_default I)
             #> (Option.map (Config.put ATP_Systems.force_sos)
                   force_sos |> the_default I))
-    val params as {relevance_thresholds, max_relevant, slice, ...} =
+    val params as {max_relevant, slice, ...} =
       Sledgehammer_Isar.default_params ctxt
          ([("verbose", "true"),
            ("type_enc", type_enc),
            ("strict", strict),
            ("lam_trans", lam_trans |> the_default lam_trans_default),

     val default_max_relevant =
       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
         prover_name
     val is_appropriate_prop =
       Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
-    val is_built_in_const =
-      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
-    val relevance_fudge =
-      Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
-    val relevance_override = {add = [], del = [], only = false}
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
     val time_limit =
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))

       let
         val _ = if is_appropriate_prop concl_t then ()
                 else raise Fail "inappropriate"
         val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
         val facts =
-          Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
-            chained_ths hyp_ts concl_t
+          Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
+              Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
           |> filter (is_appropriate_prop o prop_of o snd)
-          |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+          |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_relevant max_relevant)
-                 is_built_in_const relevance_fudge relevance_override
-                 chained_ths hyp_ts concl_t
+                 Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts
+                 concl_t
         val problem =
           {state = st', goal = goal, subgoal = i,
            subgoal_count = Sledgehammer_Util.subgoal_count st,
            facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
       in prover params (K (K (K ""))) problem end)) ()