1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 16:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 16:54:46 2010 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4         "# Cannot determine problem status within resource limit"),
     1.5        (OutOfResources, "SZS status: ResourceOut"),
     1.6        (OutOfResources, "SZS status ResourceOut")],
     1.7 -   max_new_relevant_facts_per_iter = 80 (* FIXME *),
     1.8 +   max_new_relevant_facts_per_iter = 90 (* FIXME *),
     1.9     prefers_theory_relevant = false,
    1.10     explicit_forall = false}
    1.11  val e = ("e", e_config)
    1.12 @@ -165,7 +165,7 @@
    1.13        (MalformedInput, "Undefined symbol"),
    1.14        (MalformedInput, "Free Variable"),
    1.15        (OldSpass, "tptp2dfg")],
    1.16 -   max_new_relevant_facts_per_iter = 26 (* FIXME *),
    1.17 +   max_new_relevant_facts_per_iter = 35 (* FIXME *),
    1.18     prefers_theory_relevant = true,
    1.19     explicit_forall = true}
    1.20  val spass = ("spass", spass_config)
    1.21 @@ -188,7 +188,7 @@
    1.22        (IncompleteUnprovable, "CANNOT PROVE"),
    1.23        (Unprovable, "Satisfiability detected"),
    1.24        (OutOfResources, "Refutation not found")],
    1.25 -   max_new_relevant_facts_per_iter = 40 (* FIXME *),
    1.26 +   max_new_relevant_facts_per_iter = 50 (* FIXME *),
    1.27     prefers_theory_relevant = false,
    1.28     explicit_forall = false}
    1.29  val vampire = ("vampire", vampire_config)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 16:41:32 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jul 29 16:54:46 2010 +0200
     2.3 @@ -340,7 +340,7 @@
     2.4        val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
     2.5                             Symtab.empty
     2.6        val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
     2.7 -      val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
     2.8 +      val relevance_threshold = 0.8 * relevance_threshold (* FIXME *)
     2.9        val _ =
    2.10          trace_msg (fn () => "Initial constants: " ^
    2.11                              commas (goal_const_tab