1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 09:03:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 09:23:21 2010 +0200
     1.3 @@ -255,7 +255,9 @@
     1.4  fun irrel_weight _ _ = 1.0
     1.5  *)
     1.6  
     1.7 -fun axiom_weight const_tab relevant_consts axiom_consts =
     1.8 +val chained_bonus_factor = 2.0
     1.9 +
    1.10 +fun axiom_weight chained const_tab relevant_consts axiom_consts =
    1.11    case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
    1.12                      ||> filter_out (pseudoconst_mem swap relevant_consts) of
    1.13      ([], []) => 0.0
    1.14 @@ -263,6 +265,7 @@
    1.15    | (rel, irrel) =>
    1.16      let
    1.17        val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
    1.18 +                       |> chained ? curry Real.* chained_bonus_factor
    1.19        val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
    1.20        val res = rel_weight / (rel_weight + irrel_weight)
    1.21      in if Real.isFinite res then res else 0.0 end
    1.22 @@ -395,7 +398,8 @@
    1.23                val weight =
    1.24                  case cached_weight of
    1.25                    SOME w => w
    1.26 -                | NONE => axiom_weight const_tab rel_const_tab axiom_consts
    1.27 +                | NONE => axiom_weight (snd (name ())) const_tab rel_const_tab
    1.28 +                                       axiom_consts
    1.29  (* TODO: experiment
    1.30  val _ = if String.isPrefix "lift.simps(3" (fst (name ())) then
    1.31  tracing ("*** " ^ (fst (name ())) ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))