# HG changeset patch
# User blanchet
# Date 1271429580 -7200
# Node ID 0ee736f08ed0d384b8123c4d6df36e2378f52551
# Parent  54a9c06790798e247a40b6f406430b97604f29a1
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
saves 2 sec per Sledgehammer invocation on my laptop!

diff -r 54a9c0679079 -r 0ee736f08ed0 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Apr 16 16:51:54 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Apr 16 16:53:00 2010 +0200
@@ -177,9 +177,8 @@
 
 (*The frequency of a constant is the sum of those of all instances of its type.*)
 fun const_frequency ctab (c, cts) =
-  let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
-      fun add ((cts',m), n) = if match_types cts cts' then m+n else n
-  in  List.foldl add 0 pairs  end;
+  CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
+             (the (Symtab.lookup ctab c)) 0
 
 (*Add in a constant's weight, as determined by its frequency.*)
 fun add_ct_weight ctab ((c,T), w) =
@@ -504,19 +503,23 @@
 
 fun get_relevant_facts respect_no_atp relevance_threshold convergence
                        higher_order follow_defs max_new theory_const
-                       relevance_override (ctxt, (chain_ths, th)) goal_cls =
-  let
-    val thy = ProofContext.theory_of ctxt
-    val is_FO = is_first_order thy higher_order goal_cls
-    val included_cls = get_all_lemmas respect_no_atp ctxt
-      |> cnf_rules_pairs thy |> make_unique
-      |> restrict_to_logic thy is_FO
-      |> remove_unwanted_clauses
-  in
-    relevance_filter ctxt relevance_threshold convergence follow_defs max_new
-                     theory_const relevance_override thy included_cls
-                     (map prop_of goal_cls)
-  end;
+                       (relevance_override as {add, only, ...})
+                       (ctxt, (chain_ths, th)) goal_cls =
+  if (only andalso null add) orelse relevance_threshold > 1.0 then
+    []
+  else
+    let
+      val thy = ProofContext.theory_of ctxt
+      val is_FO = is_first_order thy higher_order goal_cls
+      val included_cls = get_all_lemmas respect_no_atp ctxt
+        |> cnf_rules_pairs thy |> make_unique
+        |> restrict_to_logic thy is_FO
+        |> remove_unwanted_clauses
+    in
+      relevance_filter ctxt relevance_threshold convergence follow_defs max_new
+                       theory_const relevance_override thy included_cls
+                       (map prop_of goal_cls)
+    end
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)