diff -r eef663f8242e -r caf27e675dd1 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 02 10:16:10 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 02 12:42:05 2012 +0100 @@ -352,7 +352,8 @@ (* Experimental *) val spass_new_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass_new"), - required_execs = [], + required_execs = + [("SPASS_NEW_HOME", "SPASS"), ("SPASS_NEW_HOME", "tptp2dfg")], arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ => ("-Auto -LR=1 -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",