src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
changeset 48296 e7f01b7e244e
parent 48293 914ca0827804
child 48308 89674e5a4d35
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  signature SLEDGEHAMMER_FILTER_ITER =
     1.5  sig
     1.6    type stature = ATP_Problem_Generate.stature
     1.7 +  type fact = Sledgehammer_Fact.fact
     1.8    type params = Sledgehammer_Provers.params
     1.9    type relevance_fudge = Sledgehammer_Provers.relevance_fudge
    1.10  
    1.11 @@ -19,14 +20,14 @@
    1.12      -> string list
    1.13    val iterative_relevant_facts :
    1.14      Proof.context -> params -> string -> int -> relevance_fudge option
    1.15 -    -> term list -> term -> (((unit -> string) * stature) * thm) list
    1.16 -    -> (((unit -> string) * stature) * thm) list
    1.17 +    -> term list -> term -> fact list -> fact list
    1.18  end;
    1.19  
    1.20  structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
    1.21  struct
    1.22  
    1.23  open ATP_Problem_Generate
    1.24 +open Sledgehammer_Fact
    1.25  open Sledgehammer_Provers
    1.26  
    1.27  val trace =
    1.28 @@ -333,12 +334,9 @@
    1.29          val res = rel_weight / (rel_weight + irrel_weight)
    1.30        in if Real.isFinite res then res else 0.0 end
    1.31  
    1.32 -type annotated_thm =
    1.33 -  (((unit -> string) * stature) * thm) * (string * ptype) list
    1.34 -
    1.35  fun take_most_relevant ctxt max_facts remaining_max
    1.36          ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
    1.37 -        (candidates : (annotated_thm * real) list) =
    1.38 +        (candidates : ((fact * (string * ptype) list) * real) list) =
    1.39    let
    1.40      val max_imperfect =
    1.41        Real.ceil (Math.pow (max_imperfect,