# HG changeset patch
# User blanchet
# Date 1283373105 -7200
# Node ID a2d7be688ea148c8168e9627c1549f4d9ef073d4
# Parent  42e6eb597c30e060d52758515493194ef55453bf
add dependency of "spass" script

diff -r 42e6eb597c30 -r a2d7be688ea1 src/HOL/Tools/ATP/atp_systems.ML
--- 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))