src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

        (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 (Thm.eq_thm o pairself snd) max_facts mess, unknown) end
+  in (mesh_facts (Thm.eq_thm_prop 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

         [] |> (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 (Thm.eq_thm o pairself snd) max_facts mess
+      mesh_facts (Thm.eq_thm_prop 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"