add a bonus for chained facts, since they are likely to be relevant;
(especially in a Mirabelle run!) -- chained facts used to be included forcibly, then were treated as any other fact; the current approach seems more flexible

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 09:03:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 09:23:21 2010 +0200
@@ -255,7 +255,9 @@
 fun irrel_weight _ _ = 1.0
 *)
 
-fun axiom_weight const_tab relevant_consts axiom_consts =
+val chained_bonus_factor = 2.0
+
+fun axiom_weight chained const_tab relevant_consts axiom_consts =
   case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
                     ||> filter_out (pseudoconst_mem swap relevant_consts) of
     ([], []) => 0.0
@@ -263,6 +265,7 @@
   | (rel, irrel) =>
     let
       val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
+                       |> chained ? curry Real.* chained_bonus_factor
       val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
       val res = rel_weight / (rel_weight + irrel_weight)
     in if Real.isFinite res then res else 0.0 end
@@ -395,7 +398,8 @@
               val weight =
                 case cached_weight of
                   SOME w => w
-                | NONE => axiom_weight const_tab rel_const_tab axiom_consts
+                | NONE => axiom_weight (snd (name ())) const_tab rel_const_tab
+                                       axiom_consts
 (* TODO: experiment
 val _ = if String.isPrefix "lift.simps(3" (fst (name ())) then
 tracing ("*** " ^ (fst (name ())) ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))