if no facts were selected on first iteration, try again with a lower threshold

--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Aug 23 18:25:49 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Aug 23 18:39:12 2010 +0200
@@ -447,7 +447,7 @@
 \label{relevance-filter}
 
 \begin{enum}
-\opdefault{relevance\_threshold}{int}{50}
+\opdefault{relevance\_threshold}{int}{40}
 Specifies the threshold above which facts are considered relevant by the
 relevance filter. The option ranges from 0 to 100, where 0 means that all
 theorems are relevant.

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 18:25:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 18:39:12 2010 +0200
@@ -289,6 +289,9 @@
       end
   end;
 
+val threshold_divisor = 2.0
+val ridiculous_threshold = 0.1
+
 fun relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant
                      ({add, del, ...} : relevance_override) axioms goal_ts =
@@ -302,7 +305,6 @@
       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
                            Symtab.empty
       val goal_const_tab = get_consts_typs thy (SOME false) goal_ts
-      val relevance_threshold = 0.8 * relevance_threshold (* FIXME *)
       val _ =
         trace_msg (fn () => "Initial constants: " ^
                             commas (goal_const_tab
@@ -311,16 +313,21 @@
                                     |> map fst))
       val add_thms = maps (ProofContext.get_fact ctxt) add
       val del_thms = maps (ProofContext.get_fact ctxt) del
-      fun iter threshold rel_const_tab =
+      fun iter j threshold rel_const_tab =
         let
           fun relevant ([], rejects) [] =
-              (* Nothing was added this iteration: Add "add:" facts. *)
-              if null add_thms then
-                []
+              (* Nothing was added this iteration. *)
+              if j = 0 andalso threshold >= ridiculous_threshold then
+                (* First iteration? Try again. *)
+                iter 0 (threshold / threshold_divisor) rel_const_tab rejects
               else
-                map_filter (fn (p as (name, th), _) =>
-                               if member Thm.eq_thm add_thms th then SOME p
-                               else NONE) rejects
+                (* Add "add:" facts. *)
+                if null add_thms then
+                  []
+                else
+                  map_filter (fn (p as (name, th), _) =>
+                                 if member Thm.eq_thm add_thms th then SOME p
+                                 else NONE) rejects
             | relevant (newpairs, rejects) [] =
               let
                 val (newrels, more_rejects) = take_best max_new newpairs
@@ -332,8 +339,8 @@
               in
                 trace_msg (fn () => "relevant this iteration: " ^
                                     Int.toString (length newrels));
-                map #1 newrels @ iter threshold rel_const_tab
-                    (more_rejects @ rejects)
+                map #1 newrels @
+                iter (j + 1) threshold rel_const_tab (more_rejects @ rejects)
               end
             | relevant (newrels, rejects)
                        ((ax as ((name, th), consts_typs)) :: axs) =
@@ -356,7 +363,7 @@
                                 Real.toString threshold);
             relevant ([], [])
           end
-      val relevant = iter relevance_threshold goal_const_tab
+      val relevant = iter 0 relevance_threshold goal_const_tab
                           (map (pair_consts_typs_axiom theory_relevant thy)
                                axioms)
     in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 23 18:25:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Aug 23 18:39:12 2010 +0200
@@ -67,7 +67,7 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("explicit_apply", "false"),
-   ("relevance_threshold", "50"),
+   ("relevance_threshold", "40"),
    ("relevance_convergence", "320"),
    ("max_relevant_per_iter", "smart"),
    ("theory_relevant", "smart"),