diff -r cbc398fb30bb -r ef8d65f64f77 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 02 12:51:03 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 02 15:14:18 2012 +0100
@@ -355,7 +355,8 @@
    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))
+     ("-Auto -LR=1 -LT=1 -Isabelle=1 -TimeLimit=" ^
+      string_of_int (to_secs 1 timeout))
      |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",
    proof_delims = #proof_delims spass_config,
    known_failures = #known_failures spass_config,