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 @@ -336,14 +336,14 @@
     1.4  type annotated_thm =
     1.5    (((unit -> string) * stature) * thm) * (string * ptype) list
     1.6  
     1.7 -fun take_most_relevant ctxt max_relevant remaining_max
     1.8 +fun take_most_relevant ctxt max_facts remaining_max
     1.9          ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
    1.10          (candidates : (annotated_thm * real) list) =
    1.11    let
    1.12      val max_imperfect =
    1.13        Real.ceil (Math.pow (max_imperfect,
    1.14                      Math.pow (Real.fromInt remaining_max
    1.15 -                              / Real.fromInt max_relevant, max_imperfect_exp)))
    1.16 +                              / Real.fromInt max_facts, max_imperfect_exp)))
    1.17      val (perfect, imperfect) =
    1.18        candidates |> sort (Real.compare o swap o pairself snd)
    1.19                   |> take_prefix (fn (_, w) => w > 0.99999)
    1.20 @@ -393,7 +393,7 @@
    1.21     facts are included. *)
    1.22  val special_fact_index = 75
    1.23  
    1.24 -fun relevance_filter ctxt thres0 decay max_relevant is_built_in_const
    1.25 +fun relevance_filter ctxt thres0 decay max_facts is_built_in_const
    1.26          (fudge as {threshold_divisor, ridiculous_threshold, ...}) facts hyp_ts
    1.27          concl_t =
    1.28    let
    1.29 @@ -416,15 +416,14 @@
    1.30              (* Nothing has been added this iteration. *)
    1.31              if j = 0 andalso thres >= ridiculous_threshold then
    1.32                (* First iteration? Try again. *)
    1.33 -              iter 0 max_relevant (thres / threshold_divisor) rel_const_tab
    1.34 +              iter 0 max_facts (thres / threshold_divisor) rel_const_tab
    1.35                     hopeless hopeful
    1.36              else
    1.37                []
    1.38            | relevant candidates rejects [] =
    1.39              let
    1.40                val (accepts, more_rejects) =
    1.41 -                take_most_relevant ctxt max_relevant remaining_max fudge
    1.42 -                                   candidates
    1.43 +                take_most_relevant ctxt max_facts remaining_max fudge candidates
    1.44                val rel_const_tab' =
    1.45                  rel_const_tab
    1.46                  |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
    1.47 @@ -495,7 +494,7 @@
    1.48            val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
    1.49            val (bef, after) =
    1.50              accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
    1.51 -                    |> take (max_relevant - length add)
    1.52 +                    |> take (max_facts - length add)
    1.53                      |> chop special_fact_index
    1.54          in bef @ add @ after end
    1.55      fun insert_special_facts accepts =
    1.56 @@ -505,15 +504,15 @@
    1.57            |> insert_into_facts accepts
    1.58    in
    1.59      facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
    1.60 -          |> iter 0 max_relevant thres0 goal_const_tab []
    1.61 +          |> iter 0 max_facts thres0 goal_const_tab []
    1.62            |> insert_special_facts
    1.63            |> tap (fn accepts => trace_msg ctxt (fn () =>
    1.64                        "Total relevant: " ^ string_of_int (length accepts)))
    1.65    end
    1.66  
    1.67  fun iterative_relevant_facts ctxt
    1.68 -        ({relevance_thresholds = (thres0, thres1), ...} : params) prover
    1.69 -        max_relevant fudge hyp_ts concl_t facts =
    1.70 +        ({fact_thresholds = (thres0, thres1), ...} : params) prover
    1.71 +        max_facts fudge hyp_ts concl_t facts =
    1.72    let
    1.73      val thy = Proof_Context.theory_of ctxt
    1.74      val is_built_in_const =
    1.75 @@ -523,7 +522,7 @@
    1.76          SOME fudge => fudge
    1.77        | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
    1.78      val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
    1.79 -                          1.0 / Real.fromInt (max_relevant + 1))
    1.80 +                          1.0 / Real.fromInt (max_facts + 1))
    1.81    in
    1.82      trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
    1.83                               " facts");
    1.84 @@ -532,8 +531,8 @@
    1.85       else if thres0 > 1.0 orelse thres0 > thres1 then
    1.86         []
    1.87       else
    1.88 -       relevance_filter ctxt thres0 decay max_relevant is_built_in_const
    1.89 -           fudge facts hyp_ts
    1.90 +       relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
    1.91 +           facts hyp_ts
    1.92             (concl_t |> theory_constify fudge (Context.theory_name thy)))
    1.93    end
    1.94