diff -r 4d5bbec1a598 -r 8fe717f5048e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Aug 22 22:47:03 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 23 00:09:25 2010 +0200
@@ -149,7 +149,7 @@
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   default_max_relevant_per_iter = 50 (* FIXME *),
+   default_max_relevant_per_iter = 50 (* FUDGE *),
    default_theory_relevant = false,
    explicit_forall = false,
    use_conjecture_for_hypotheses = true}
@@ -162,7 +162,6 @@
 val spass_config : prover_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS")],
-   (* "div 2" accounts for the fact that SPASS is often run twice. *)
    arguments = fn complete => fn timeout =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
@@ -177,7 +176,7 @@
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
       (SpassTooOld, "tptp2dfg")],
-   default_max_relevant_per_iter = 35 (* FIXME *),
+   default_max_relevant_per_iter = 32 (* FUDGE *),
    default_theory_relevant = true,
    explicit_forall = true,
    use_conjecture_for_hypotheses = true}
@@ -205,7 +204,7 @@
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (VampireTooOld, "not a valid option")],
-   default_max_relevant_per_iter = 45 (* FIXME *),
+   default_max_relevant_per_iter = 45 (* FUDGE *),
    default_theory_relevant = false,
    explicit_forall = false,
    use_conjecture_for_hypotheses = true}
@@ -279,10 +278,10 @@
 val remote_vampire = remotify_prover vampire "Vampire---9"
 val remote_sine_e =
   remote_prover "sine_e" "SInE---" []
-                [(Unprovable, "says Unknown")] 150 (* FIXME *) false true
+                [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
 val remote_snark =
   remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
-                50 (* FIXME *) false true
+                50 (* FUDGE *) false true
 
 (* Setup *)