# HG changeset patch
# User blanchet
# Date 1280415286 -7200
# Node ID fe51c098b0ab5cb1fd16c19aec4ffd51e526e2c4
# Parent  ed65a0777e10b18ad61a8f26ebb24abcea3f799b
fiddle with the fudge factors, to get similar results as before

diff -r ed65a0777e10 -r fe51c098b0ab src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 16:41:32 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 16:54:46 2010 +0200
@@ -139,7 +139,7 @@
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   max_new_relevant_facts_per_iter = 80 (* FIXME *),
+   max_new_relevant_facts_per_iter = 90 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
 val e = ("e", e_config)
@@ -165,7 +165,7 @@
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
       (OldSpass, "tptp2dfg")],
-   max_new_relevant_facts_per_iter = 26 (* FIXME *),
+   max_new_relevant_facts_per_iter = 35 (* FIXME *),
    prefers_theory_relevant = true,
    explicit_forall = true}
 val spass = ("spass", spass_config)
@@ -188,7 +188,7 @@
       (IncompleteUnprovable, "CANNOT PROVE"),
       (Unprovable, "Satisfiability detected"),
       (OutOfResources, "Refutation not found")],
-   max_new_relevant_facts_per_iter = 40 (* FIXME *),
+   max_new_relevant_facts_per_iter = 50 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
 val vampire = ("vampire", vampire_config)
diff -r ed65a0777e10 -r fe51c098b0ab src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 16:41:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 16:54:46 2010 +0200
@@ -340,7 +340,7 @@
       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
                            Symtab.empty
       val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
-      val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
+      val relevance_threshold = 0.8 * relevance_threshold (* FIXME *)
       val _ =
         trace_msg (fn () => "Initial constants: " ^
                             commas (goal_const_tab