--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 01 21:47:25 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 01 22:31:45 2010 +0200
@@ -168,7 +168,7 @@
counteracting the presence of "hAPP". *)
val spass_config : prover_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
- required_execs = [("SPASS_HOME", "SPASS")],
+ required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
arguments = fn complete => fn timeout =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))