src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

     -> (string * real) list
   val isar_dependencies_of : string Symtab.table -> thm -> string list option
   val prover_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> string Symtab.table
     -> thm -> bool * string list option
-  val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
+  val weight_mash_facts : 'a list -> ('a * real) list
   val find_mash_suggestions :
     int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list
     -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
   val mash_suggested_facts :
     Proof.context -> params -> string -> int -> term list -> term -> fact list

   in find_maxes Symtab.empty ([], Graph.maximals fact_G) end
 
 fun is_fact_in_graph fact_G (_, th) =
   can (Graph.get_node fact_G) (nickname_of th)
 
-(* use MePo weights for now *)
 val weight_raw_mash_facts = weight_mepo_facts
 val weight_mash_facts = weight_raw_mash_facts
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =