# HG changeset patch
# User blanchet
# Date 1287751663 -7200
# Node ID bdb890782d4acba0c5363c1c176e30c11603d8e9
# Parent  6f7bf79b1506e56558885bbe11b4ed94aa5a8492
replaced references with proper record that's threaded through

diff -r 6f7bf79b1506 -r bdb890782d4a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 22 14:10:32 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 22 14:47:43 2010 +0200
@@ -350,13 +350,14 @@
     val params as {full_types, relevance_thresholds, max_relevant, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("timeout", Int.toString timeout ^ " s")]
-    val relevance_override = {add = [], del = [], only = false}
     val default_max_relevant =
       Sledgehammer.default_max_relevant_for_prover thy prover_name
+    val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name
+    val relevance_override = {add = [], del = [], only = false}
     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     val axioms =
       Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
-          (the_default default_max_relevant max_relevant)
+          (the_default default_max_relevant max_relevant) relevance_fudge
           relevance_override chained_ths hyp_ts concl_t
     val problem =
       {state = st', goal = goal, subgoal = i,
diff -r 6f7bf79b1506 -r bdb890782d4a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Oct 22 14:10:32 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Oct 22 14:47:43 2010 +0200
@@ -5,26 +5,37 @@
 structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION =
 struct
 
-structure SF = Sledgehammer_Filter
+fun get args name default_value =
+  case AList.lookup (op =) args name of
+    SOME value => the (Real.fromString value)
+  | NONE => default_value
 
-val relevance_filter_args =
-  [("worse_irrel_freq", SF.worse_irrel_freq),
-   ("higher_order_irrel_weight", SF.higher_order_irrel_weight),
-   ("abs_rel_weight", SF.abs_rel_weight),
-   ("abs_irrel_weight", SF.abs_irrel_weight),
-   ("skolem_irrel_weight", SF.skolem_irrel_weight),
-   ("theory_const_rel_weight", SF.theory_const_rel_weight),
-   ("theory_const_irrel_weight", SF.theory_const_irrel_weight),
-   ("intro_bonus", SF.intro_bonus),
-   ("elim_bonus", SF.elim_bonus),
-   ("simp_bonus", SF.simp_bonus),
-   ("local_bonus", SF.local_bonus),
-   ("assum_bonus", SF.assum_bonus),
-   ("chained_bonus", SF.chained_bonus),
-   ("max_imperfect", SF.max_imperfect),
-   ("max_imperfect_exp", SF.max_imperfect_exp),
-   ("threshold_divisor", SF.threshold_divisor),
-   ("ridiculous_threshold", SF.ridiculous_threshold)]
+fun extract_relevance_fudge args
+      {worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
+       abs_irrel_weight, skolem_irrel_weight, theory_const_rel_weight,
+       theory_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
+       local_bonus, assum_bonus, chained_bonus, max_imperfect,
+       max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
+  {worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
+   higher_order_irrel_weight =
+       get args "higher_order_irrel_weight" higher_order_irrel_weight,
+   abs_rel_weight = get args "abs_rel_weight" abs_rel_weight,
+   abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight,
+   skolem_irrel_weight = get args "skolem_irrel_weight" skolem_irrel_weight,
+   theory_const_rel_weight =
+       get args "theory_const_rel_weight" theory_const_rel_weight,
+   theory_const_irrel_weight =
+       get args "theory_const_irrel_weight" theory_const_irrel_weight,
+   intro_bonus = get args "intro_bonus" intro_bonus,
+   elim_bonus = get args "elim_bonus" elim_bonus,
+   simp_bonus = get args "simp_bonus" simp_bonus,
+   local_bonus = get args "local_bonus" local_bonus,
+   assum_bonus = get args "assum_bonus" assum_bonus,
+   chained_bonus = get args "chained_bonus" chained_bonus,
+   max_imperfect = get args "max_imperfect" max_imperfect,
+   max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp,
+   threshold_divisor = get args "threshold_divisor" threshold_divisor,
+   ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold}
 
 structure Prooftab =
   Table(type key = int * int val ord = prod_ord int_ord int_ord);
@@ -85,6 +96,7 @@
     ()
 
 val default_max_relevant = 300
+val prover_name = ATP_Systems.eN (* arbitrary ATP *)
 
 fun with_index (i, s) = s ^ "@" ^ string_of_int i
 
@@ -95,21 +107,17 @@
        SOME proofs =>
        let
          val {context = ctxt, facts, goal} = Proof.goal pre
-         val args =
-           args
-           |> filter (fn (key, value) =>
-                         case AList.lookup (op =) relevance_filter_args key of
-                           SOME rf => (rf := the (Real.fromString value); false)
-                         | NONE => true)
-
+         val relevance_fudge =
+           extract_relevance_fudge args
+               (Sledgehammer.relevance_fudge_for_prover prover_name)
          val {relevance_thresholds, full_types, max_relevant, ...} =
            Sledgehammer_Isar.default_params ctxt args
          val subgoal = 1
          val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
          val facts =
-           SF.relevant_facts ctxt full_types
+           Sledgehammer_Filter.relevant_facts ctxt full_types
                relevance_thresholds
-               (the_default default_max_relevant max_relevant)
+               (the_default default_max_relevant max_relevant) relevance_fudge
                {add = [], del = [], only = false} facts hyp_ts concl_t
            |> map (fst o fst)
          val (found_facts, lost_facts) =
diff -r 6f7bf79b1506 -r bdb890782d4a src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 14:10:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 14:47:43 2010 +0200
@@ -10,6 +10,7 @@
 sig
   type failure = ATP_Systems.failure
   type locality = Sledgehammer_Filter.locality
+  type relevance_fudge = Sledgehammer_Filter.relevance_fudge
   type relevance_override = Sledgehammer_Filter.relevance_override
   type prepared_formula = Sledgehammer_ATP_Translate.prepared_formula
   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
@@ -51,6 +52,7 @@
 
   val smtN : string
   val default_max_relevant_for_prover : theory -> string -> int
+  val relevance_fudge_for_prover : string -> relevance_fudge
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
@@ -87,13 +89,58 @@
 val smtN = "smt"
 val smt_prover_names = [smtN, remote_prefix ^ smtN]
 
+val is_smt_prover = member (op =) smt_prover_names
+
 val smt_default_max_relevant = 300 (* FUDGE *)
 val auto_max_relevant_divisor = 2 (* FUDGE *)
 
 fun default_max_relevant_for_prover thy name =
-  if member (op =) smt_prover_names name then smt_default_max_relevant
+  if is_smt_prover name then smt_default_max_relevant
   else #default_max_relevant (get_atp thy name)
 
+(* FUDGE *)
+val atp_relevance_fudge =
+  {worse_irrel_freq = 100.0,
+   higher_order_irrel_weight = 1.05,
+   abs_rel_weight = 0.5,
+   abs_irrel_weight = 2.0,
+   skolem_irrel_weight = 0.75,
+   theory_const_rel_weight = 0.5,
+   theory_const_irrel_weight = 0.25,
+   intro_bonus = 0.15,
+   elim_bonus = 0.15,
+   simp_bonus = 0.15,
+   local_bonus = 0.55,
+   assum_bonus = 1.05,
+   chained_bonus = 1.5,
+   max_imperfect = 11.5,
+   max_imperfect_exp = 1.0,
+   threshold_divisor = 2.0,
+   ridiculous_threshold = 0.1}
+
+(* FUDGE *)
+val smt_relevance_fudge =
+  {worse_irrel_freq = 100.0,
+   higher_order_irrel_weight = 1.05,
+   abs_rel_weight = 0.5,
+   abs_irrel_weight = 2.0,
+   skolem_irrel_weight = 0.75,
+   theory_const_rel_weight = 0.5,
+   theory_const_irrel_weight = 0.25,
+   intro_bonus = 0.15,
+   elim_bonus = 0.15,
+   simp_bonus = 0.15,
+   local_bonus = 0.55,
+   assum_bonus = 1.05,
+   chained_bonus = 1.5,
+   max_imperfect = 11.5,
+   max_imperfect_exp = 1.0,
+   threshold_divisor = 2.0,
+   ridiculous_threshold = 0.1}
+
+fun relevance_fudge_for_prover name =
+  if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge
+
 fun available_provers thy =
   let
     val (remote_provers, local_provers) =
@@ -364,10 +411,8 @@
   end
 
 fun get_prover thy auto name =
-  if member (op =) smt_prover_names name then
-    run_smt_solver (String.isPrefix remote_prefix)
-  else
-    run_atp auto name (get_atp thy name)
+  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix)
+  else run_atp auto name (get_atp thy name)
 
 fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
                auto minimize_command
@@ -439,9 +484,9 @@
       val (_, hyp_ts, concl_t) = strip_subgoal goal i
       val _ = () |> not blocking ? kill_provers
       val _ = if auto then () else priority "Sledgehammering..."
-      val (smts, atps) =
-        provers |> List.partition (member (op =) smt_prover_names)
-      fun run_provers full_types maybe_prepare provers (res as (success, state)) =
+      val (smts, atps) = provers |> List.partition is_smt_prover
+      fun run_provers full_types relevance_fudge maybe_prepare provers
+                      (res as (success, state)) =
         if success orelse null provers then
           res
         else
@@ -455,8 +500,8 @@
                   |> auto ? (fn n => n div auto_max_relevant_divisor)
             val axioms =
               relevant_facts ctxt full_types relevance_thresholds
-                             max_max_relevant relevance_override chained_ths
-                             hyp_ts concl_t
+                             max_max_relevant relevance_fudge relevance_override
+                             chained_ths hyp_ts concl_t
               |> map maybe_prepare
             val problem =
               {state = state, goal = goal, subgoal = i, subgoal_count = n,
@@ -472,8 +517,9 @@
                              (run_prover problem)
                       |> exists fst |> rpair state
           end
-      val run_atps = run_provers full_types (Prepared o prepare_axiom ctxt) atps
-      val run_smts = run_provers true Unprepared smts
+      val run_atps = run_provers full_types atp_relevance_fudge
+                                 (Prepared o prepare_axiom ctxt) atps
+      val run_smts = run_provers true smt_relevance_fudge Unprepared smts
       fun run_atps_and_smt_solvers () =
         [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
     in
diff -r 6f7bf79b1506 -r bdb890782d4a src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Oct 22 14:10:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Oct 22 14:47:43 2010 +0200
@@ -9,35 +9,38 @@
 sig
   datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
+  type relevance_fudge =
+    {worse_irrel_freq : real,
+     higher_order_irrel_weight : real,
+     abs_rel_weight : real,
+     abs_irrel_weight : real,
+     skolem_irrel_weight : real,
+     theory_const_rel_weight : real,
+     theory_const_irrel_weight : real,
+     intro_bonus : real,
+     elim_bonus : real,
+     simp_bonus : real,
+     local_bonus : real,
+     assum_bonus : real,
+     chained_bonus : real,
+     max_imperfect : real,
+     max_imperfect_exp : real,
+     threshold_divisor : real,
+     ridiculous_threshold : real}
+
   type relevance_override =
-    {add: (Facts.ref * Attrib.src list) list,
-     del: (Facts.ref * Attrib.src list) list,
-     only: bool}
+    {add : (Facts.ref * Attrib.src list) list,
+     del : (Facts.ref * Attrib.src list) list,
+     only : bool}
 
   val trace : bool Unsynchronized.ref
-  val worse_irrel_freq : real Unsynchronized.ref
-  val higher_order_irrel_weight : real Unsynchronized.ref
-  val abs_rel_weight : real Unsynchronized.ref
-  val abs_irrel_weight : real Unsynchronized.ref
-  val skolem_irrel_weight : real Unsynchronized.ref
-  val theory_const_rel_weight : real Unsynchronized.ref
-  val theory_const_irrel_weight : real Unsynchronized.ref
-  val intro_bonus : real Unsynchronized.ref
-  val elim_bonus : real Unsynchronized.ref
-  val simp_bonus : real Unsynchronized.ref
-  val local_bonus : real Unsynchronized.ref
-  val assum_bonus : real Unsynchronized.ref
-  val chained_bonus : real Unsynchronized.ref
-  val max_imperfect : real Unsynchronized.ref
-  val max_imperfect_exp : real Unsynchronized.ref
-  val threshold_divisor : real Unsynchronized.ref
-  val ridiculous_threshold : real Unsynchronized.ref
   val name_thm_pairs_from_ref :
     Proof.context -> unit Symtab.table -> thm list
     -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
   val relevant_facts :
-    Proof.context -> bool -> real * real -> int -> relevance_override
-    -> thm list -> term list -> term -> ((string * locality) * thm) list
+    Proof.context -> bool -> real * real -> int -> relevance_fudge
+    -> relevance_override -> thm list -> term list -> term
+    -> ((string * locality) * thm) list
 end;
 
 structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
@@ -52,31 +55,31 @@
 val term_patterns = false
 val respect_no_atp = true
 
-(* FUDGE *)
-val worse_irrel_freq = Unsynchronized.ref 100.0
-val higher_order_irrel_weight = Unsynchronized.ref 1.05
-val abs_rel_weight = Unsynchronized.ref 0.5
-val abs_irrel_weight = Unsynchronized.ref 2.0
-val skolem_irrel_weight = Unsynchronized.ref 0.75
-val theory_const_rel_weight = Unsynchronized.ref 0.5
-val theory_const_irrel_weight = Unsynchronized.ref 0.25
-val intro_bonus = Unsynchronized.ref 0.15
-val elim_bonus = Unsynchronized.ref 0.15
-val simp_bonus = Unsynchronized.ref 0.15
-val local_bonus = Unsynchronized.ref 0.55
-val assum_bonus = Unsynchronized.ref 1.05
-val chained_bonus = Unsynchronized.ref 1.5
-val max_imperfect = Unsynchronized.ref 11.5
-val max_imperfect_exp = Unsynchronized.ref 1.0
-val threshold_divisor = Unsynchronized.ref 2.0
-val ridiculous_threshold = Unsynchronized.ref 0.1
-
 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
+type relevance_fudge =
+  {worse_irrel_freq : real,
+   higher_order_irrel_weight : real,
+   abs_rel_weight : real,
+   abs_irrel_weight : real,
+   skolem_irrel_weight : real,
+   theory_const_rel_weight : real,
+   theory_const_irrel_weight : real,
+   intro_bonus : real,
+   elim_bonus : real,
+   simp_bonus : real,
+   local_bonus : real,
+   assum_bonus : real,
+   chained_bonus : real,
+   max_imperfect : real,
+   max_imperfect_exp : real,
+   threshold_divisor : real,
+   ridiculous_threshold : real}
+
 type relevance_override =
-  {add: (Facts.ref * Attrib.src list) list,
-   del: (Facts.ref * Attrib.src list) list,
-   only: bool}
+  {add : (Facts.ref * Attrib.src list) list,
+   del : (Facts.ref * Attrib.src list) list,
+   only : bool}
 
 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
 val abs_name = sledgehammer_prefix ^ "abs"
@@ -254,9 +257,11 @@
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   takes the given theory into account.*)
-fun theory_const_prop_of th =
-  if exists (curry (op <) 0.0) [!theory_const_rel_weight,
-                                !theory_const_irrel_weight] then
+fun theory_const_prop_of ({theory_const_rel_weight,
+                           theory_const_irrel_weight, ...} : relevance_fudge)
+                         th =
+  if exists (curry (op <) 0.0) [theory_const_rel_weight,
+                                theory_const_irrel_weight] then
     let
       val name = Context.theory_name (theory_of_thm th)
       val t = Const (name ^ theory_const_suffix, @{typ bool})
@@ -282,7 +287,7 @@
 
 structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
 
-fun count_axiom_consts thy =
+fun count_axiom_consts thy fudge =
   let
     fun do_const const (s, T) ts =
       (* Two-dimensional table update. Constant maps to types maps to count. *)
@@ -295,7 +300,7 @@
       | (Free x, ts) => do_const false x ts
       | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
       | (_, ts) => fold do_term ts
-  in do_term o theory_const_prop_of o snd end
+  in do_term o theory_const_prop_of fudge o snd end
 
 
 (**** Actual Filtering Code ****)
@@ -322,11 +327,12 @@
    very rare constants and very common ones -- the former because they can't
    lead to the inclusion of too many new facts, and the latter because they are
    so common as to be of little interest. *)
-fun irrel_weight_for order freq =
-  let val (k, x) = !worse_irrel_freq |> `Real.ceil in
+fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
+                      : relevance_fudge) order freq =
+  let val (k, x) = worse_irrel_freq |> `Real.ceil in
     (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
      else rel_weight_for order freq / rel_weight_for order k)
-    * pow_int (!higher_order_irrel_weight) (order - 1)
+    * pow_int higher_order_irrel_weight (order - 1)
   end
 
 (* Computes a constant's weight, as determined by its frequency. *)
@@ -337,22 +343,25 @@
   else if String.isSuffix theory_const_suffix s then theory_const_weight
   else weight_for m (pconst_freq (match_ptype o f) const_tab c)
 
-fun rel_pconst_weight const_tab =
-  generic_pconst_weight (!abs_rel_weight) 0.0 (!theory_const_rel_weight)
+fun rel_pconst_weight ({abs_rel_weight, theory_const_rel_weight, ...}
+                       : relevance_fudge) const_tab =
+  generic_pconst_weight abs_rel_weight 0.0 theory_const_rel_weight
                         rel_weight_for I const_tab
-fun irrel_pconst_weight const_tab =
-  generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
-                    (!theory_const_irrel_weight) irrel_weight_for swap const_tab
+fun irrel_pconst_weight (fudge as {abs_irrel_weight, skolem_irrel_weight,
+                                   theory_const_irrel_weight, ...}) const_tab =
+  generic_pconst_weight abs_irrel_weight skolem_irrel_weight
+                        theory_const_irrel_weight (irrel_weight_for fudge) swap
+                        const_tab
 
-fun locality_bonus General = 0.0
-  | locality_bonus Intro = !intro_bonus
-  | locality_bonus Elim = !elim_bonus
-  | locality_bonus Simp = !simp_bonus
-  | locality_bonus Local = !local_bonus
-  | locality_bonus Assum = !assum_bonus
-  | locality_bonus Chained = !chained_bonus
+fun locality_bonus (_ : relevance_fudge) General = 0.0
+  | locality_bonus {intro_bonus, ...} Intro = intro_bonus
+  | locality_bonus {elim_bonus, ...} Elim = elim_bonus
+  | locality_bonus {simp_bonus, ...} Simp = simp_bonus
+  | locality_bonus {local_bonus, ...} Local = local_bonus
+  | locality_bonus {assum_bonus, ...} Assum = assum_bonus
+  | locality_bonus {chained_bonus, ...} Chained = chained_bonus
 
-fun axiom_weight loc const_tab relevant_consts axiom_consts =
+fun axiom_weight fudge loc const_tab relevant_consts axiom_consts =
   case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
                     ||> filter_out (pconst_hyper_mem swap relevant_consts) of
     ([], _) => 0.0
@@ -360,15 +369,15 @@
     let
       val irrel = irrel |> filter_out (pconst_mem swap rel)
       val rel_weight =
-        0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
+        0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
       val irrel_weight =
-        ~ (locality_bonus loc)
-        |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+        ~ (locality_bonus fudge loc)
+        |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
       val res = rel_weight / (rel_weight + irrel_weight)
     in if Real.isFinite res then res else 0.0 end
 
 (* FIXME: experiment
-fun debug_axiom_weight loc const_tab relevant_consts axiom_consts =
+fun debug_axiom_weight fudge loc const_tab relevant_consts axiom_consts =
   case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
                     ||> filter_out (pconst_hyper_mem swap relevant_consts) of
     ([], _) => 0.0
@@ -378,10 +387,10 @@
       val rels_weight =
         0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
       val irrels_weight =
-        ~ (locality_bonus loc)
-        |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+        ~ (locality_bonus fudge loc)
+        |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
 val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel))
-val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel))
+val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight fudge const_tab)) irrel))
       val res = rels_weight / (rels_weight + irrels_weight)
     in if Real.isFinite res then res else 0.0 end
 *)
@@ -389,8 +398,8 @@
 fun pconsts_in_axiom thy t =
   Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
               (pconsts_in_terms thy true (SOME true) [t]) []
-fun pair_consts_axiom thy axiom =
-  case axiom |> snd |> theory_const_prop_of |> pconsts_in_axiom thy of
+fun pair_consts_axiom thy fudge axiom =
+  case axiom |> snd |> theory_const_prop_of fudge |> pconsts_in_axiom thy of
     [] => NONE
   | consts => SOME ((axiom, consts), NONE)
 
@@ -398,12 +407,13 @@
   (((unit -> string) * locality) * thm) * (string * ptype) list
 
 fun take_most_relevant max_relevant remaining_max
-                       (candidates : (annotated_thm * real) list) =
+        ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge) 
+        (candidates : (annotated_thm * real) list) =
   let
     val max_imperfect =
-      Real.ceil (Math.pow (!max_imperfect,
+      Real.ceil (Math.pow (max_imperfect,
                     Math.pow (Real.fromInt remaining_max
-                              / Real.fromInt max_relevant, !max_imperfect_exp)))
+                              / Real.fromInt max_relevant, max_imperfect_exp)))
     val (perfect, imperfect) =
       candidates |> sort (Real.compare o swap o pairself snd)
                  |> take_prefix (fn (_, w) => w > 0.99999)
@@ -428,10 +438,11 @@
     tab
 
 fun relevance_filter ctxt threshold0 decay max_relevant
-                     ({add, del, ...} : relevance_override) axioms goal_ts =
+        (fudge as {threshold_divisor, ridiculous_threshold, ...})
+        ({add, del, ...} : relevance_override) axioms goal_ts =
   let
     val thy = ProofContext.theory_of ctxt
-    val const_tab = fold (count_axiom_consts thy) axioms Symtab.empty
+    val const_tab = fold (count_axiom_consts thy fudge) axioms Symtab.empty
     val goal_const_tab =
       pconsts_in_terms thy false (SOME false) goal_ts
       |> fold (if_empty_replace_with_locality thy axioms)
@@ -450,16 +461,16 @@
                            else NONE) rejects
         fun relevant [] rejects [] =
             (* Nothing has been added this iteration. *)
-            if j = 0 andalso threshold >= !ridiculous_threshold then
+            if j = 0 andalso threshold >= ridiculous_threshold then
               (* First iteration? Try again. *)
-              iter 0 max_relevant (threshold / !threshold_divisor) rel_const_tab
+              iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
                    hopeless hopeful
             else
               game_over (rejects @ hopeless)
           | relevant candidates rejects [] =
             let
               val (accepts, more_rejects) =
-                take_most_relevant max_relevant remaining_max candidates
+                take_most_relevant max_relevant remaining_max fudge candidates
               val rel_const_tab' =
                 rel_const_tab
                 |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
@@ -499,11 +510,12 @@
               val weight =
                 case cached_weight of
                   SOME w => w
-                | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
+                | NONE => axiom_weight fudge loc const_tab rel_const_tab
+                                       axiom_consts
 (* FIXME: experiment
 val name = fst (fst (fst ax)) ()
 val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then
-tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
+tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight fudge loc const_tab rel_const_tab axiom_consts))
 else
 ()
 *)
@@ -524,7 +536,7 @@
         end
   in
     axioms |> filter_out (member Thm.eq_thm del_ths o snd)
-           |> map_filter (pair_consts_axiom thy)
+           |> map_filter (pair_consts_axiom thy fudge)
            |> iter 0 max_relevant threshold0 goal_const_tab []
            |> tap (fn res => trace_msg (fn () =>
                                 "Total relevant: " ^ Int.toString (length res)))
@@ -708,7 +720,9 @@
           (Term.add_vars t [] |> sort_wrt (fst o fst))
   |> fst
 
-fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths =
+fun all_name_thms_pairs ctxt reserved full_types
+        ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths
+        chained_ths =
   let
     val thy = ProofContext.theory_of ctxt
     val global_facts = Global_Theory.facts_of thy
@@ -718,7 +732,7 @@
     fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
     val is_chained = member Thm.eq_thm chained_ths
     val (intros, elims, simps) =
-      if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then
+      if exists (curry (op <) 0.0) [intro_bonus, elim_bonus, simp_bonus] then
         clasimpset_rules_of ctxt
       else
         (Termtab.empty, Termtab.empty, Termtab.empty)
@@ -800,9 +814,8 @@
 (* ATP invocation methods setup                                *)
 (***************************************************************)
 
-fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
-                   (relevance_override as {add, only, ...}) chained_ths hyp_ts
-                   concl_t =
+fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant fudge
+                   (override as {add, only, ...}) chained_ths hyp_ts concl_t =
   let
     val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
                           1.0 / Real.fromInt (max_relevant + 1))
@@ -813,7 +826,7 @@
          maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
                o name_thm_pairs_from_ref ctxt reserved chained_ths) add
        else
-         all_name_thms_pairs ctxt reserved full_types add_ths chained_ths)
+         all_name_thms_pairs ctxt reserved full_types fudge add_ths chained_ths)
       |> name_thm_pairs ctxt (respect_no_atp andalso not only)
       |> uniquify
   in
@@ -825,8 +838,8 @@
              max_relevant = 0 then
        []
      else
-       relevance_filter ctxt threshold0 decay max_relevant relevance_override
-                        axioms (concl_t :: hyp_ts))
+       relevance_filter ctxt threshold0 decay max_relevant fudge override axioms
+                        (concl_t :: hyp_ts))
     |> map (apfst (apfst (fn f => f ())))
   end