src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   type stature = ATP_Problem_Generate.stature
   type raw_fact = Sledgehammer_Fact.raw_fact
   type fact = Sledgehammer_Fact.fact
   type fact_override = Sledgehammer_Fact.fact_override
   type params = Sledgehammer_Provers.params
-  type relevance_fudge = Sledgehammer_Provers.relevance_fudge
   type prover_result = Sledgehammer_Provers.prover_result
 
   val trace : bool Config.T
   val MePoN : string
   val MaShN : string

         else case find_first (is_dep dep) facts of
           SOME ((_, status), th) => accum @ [(("", status), th)]
         | NONE => accum (* shouldn't happen *)
       val facts =
         facts
-        |> mepo_suggested_facts ctxt params prover
-               (max_facts |> the_default prover_default_max_facts) NONE hyp_ts
-               concl_t
+        |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
+             hyp_ts concl_t
         |> fold (add_isar_dep facts) isar_deps
         |> map nickify
     in
       if verbose andalso auto_level = 0 then
         let val num_facts = length facts in

            [] => accepts
          | _ => (facts |> filter in_add |> map fact_of_raw_fact) @
                 (accepts |> filter_out in_add))
         |> take max_facts
       fun mepo () =
-        (mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t facts
+        (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t facts
          |> weight_facts_steeply, [])
       fun mash () =
         mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts
         |>> weight_facts_steeply
       val mess =