1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Sat Oct 29 13:15:58 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Sat Oct 29 13:15:58 2011 +0200
     1.3 @@ -724,7 +724,8 @@
     1.4  
     1.5  \item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
     1.6  higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
     1.7 -with support for the TPTP many-typed higher-order syntax (THF0).
     1.8 +with support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer
     1.9 +requires version 1.2.9 or above.
    1.10  
    1.11  \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
    1.12  the external provers, Metis itself can be used for proof search.

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Oct 29 13:15:58 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Oct 29 13:15:58 2011 +0200
     2.3 @@ -255,7 +255,7 @@
     2.4     required_execs = [],
     2.5     arguments =
     2.6       fn _ => fn _ => fn sos => fn timeout => fn _ =>
     2.7 -        "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
     2.8 +        "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
     2.9          |> sos = sosN ? prefix "--sos ",
    2.10     proof_delims = tstp_proof_delims,
    2.11     known_failures =