src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   val mash_unlearn : Proof.context -> unit
   val nickname_of_thm : thm -> string
   val find_suggested_facts :
     (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
   val mesh_facts :
-    int -> (real * ((('a * thm) * real) list * ('a * thm) list)) list
-    -> ('a * thm) list
+    ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
+    -> 'a list
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
   val goal_of_thm : theory -> thm -> thm
   val run_prover_for_mash :
     Proof.context -> params -> string -> fact list -> thm -> prover_result

   val mash_learn :
     Proof.context -> params -> fact_override -> thm list -> bool -> unit
   val is_mash_enabled : unit -> bool
   val mash_can_suggest_facts : Proof.context -> bool
   val generous_max_facts : int -> int
+  val mepo_weight : real
+  val mash_weight : real
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
     -> term -> fact list -> fact list
   val kill_learners : unit -> unit
   val running_learners : unit -> unit

   | normalize_scores max_facts xs =
     let val avg = avg (map snd (take max_facts xs)) in
       map (apsnd (curry Real.* (1.0 / avg))) xs
     end
 
-fun mesh_facts max_facts [(_, (sels, unks))] =
+fun mesh_facts _ max_facts [(_, (sels, unks))] =
     map fst (take max_facts sels) @ take (max_facts - length sels) unks
-  | mesh_facts max_facts mess =
+  | mesh_facts eq max_facts mess =
     let
       val mess =
         mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
-      val fact_eq = Thm.eq_thm o pairself snd
+      val fact_eq = eq
       fun score_in fact (global_weight, ((sel_len, sels), unks)) =
         let
           fun score_at j =
             case try (nth sels) j of
               SOME (_, score) => SOME (global_weight * score)

        (0.16 (* FUDGE *), (weight_raw_mash_facts raw_mash, raw_unknown)),
        (0.04 (* FUDGE *), (weight_proximity_facts proximity, []))]
     val unknown =
       raw_unknown
       |> fold (subtract (Thm.eq_thm_prop o pairself snd)) [chained, proximity]
-  in (mesh_facts max_facts mess, unknown) end
+  in (mesh_facts (Thm.eq_thm o pairself snd) max_facts mess, unknown) end
 
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt

 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons. *)
 fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts div 2)
 
+val mepo_weight = 0.5
+val mash_weight = 0.5
+
 (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    Sledgehammer and Try. *)
 val min_secs_for_learning = 15
 
 fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover

       fun mash () =
         mash_suggested_facts ctxt params prover (generous_max_facts max_facts)
             hyp_ts concl_t facts
         |>> weight_mash_facts
       val mess =
-        [] |> (if fact_filter <> mashN then cons (0.5, (mepo (), [])) else I)
-           |> (if fact_filter <> mepoN then cons (0.5, (mash ())) else I)
+        [] |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
+               else I)
+           |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
+               else I)
     in
-      mesh_facts max_facts mess
+      mesh_facts (Thm.eq_thm o pairself snd) max_facts mess
       |> not (null add_ths) ? prepend_facts add_ths
     end
 
 fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
 fun running_learners () = Async_Manager.running_threads MaShN "learner"