src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML

 *)
 
 signature SLEDGEHAMMER_MEPO =
 sig
   type stature = ATP_Problem_Generate.stature
+  type raw_fact = Sledgehammer_Fact.raw_fact
   type fact = Sledgehammer_Fact.fact
   type params = Sledgehammer_Provers.params
   type relevance_fudge = Sledgehammer_Provers.relevance_fudge
 
   val trace : bool Config.T

   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string list
   val mepo_suggested_facts :
     Proof.context -> params -> string -> int -> relevance_fudge option
-    -> term list -> term -> fact list -> fact list
+    -> term list -> term -> raw_fact list -> fact list
 end;
 
 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
 struct
 

         val res = rel_weight / (rel_weight + irrel_weight)
       in if Real.isFinite res then res else 0.0 end
 
 fun take_most_relevant ctxt max_facts remaining_max
         ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
-        (candidates : ((fact * (string * ptype) list) * real) list) =
+        (candidates : ((raw_fact * (string * ptype) list) * real) list) =
   let
     val max_imperfect =
       Real.ceil (Math.pow (max_imperfect,
                     Math.pow (Real.fromInt remaining_max
                               / Real.fromInt max_facts, max_imperfect_exp)))

        []
      else
        relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
            facts hyp_ts
            (concl_t |> theory_constify fudge (Context.theory_name thy)))
+    |> map fact_of_raw_fact
   end
 
 end;