1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Sat Oct 29 13:15:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Sat Oct 29 13:15:58 2011 +0200
     1.3 @@ -24,8 +24,6 @@
     1.4      TimedOut |
     1.5      Inappropriate |
     1.6      OutOfResources |
     1.7 -    SpassTooOld |
     1.8 -    VampireTooOld |
     1.9      NoPerl |
    1.10      NoLibwwwPerl |
    1.11      MalformedInput |
    1.12 @@ -81,8 +79,6 @@
    1.13    TimedOut |
    1.14    Inappropriate |
    1.15    OutOfResources |
    1.16 -  SpassTooOld |
    1.17 -  VampireTooOld |
    1.18    NoPerl |
    1.19    NoLibwwwPerl |
    1.20    MalformedInput |
    1.21 @@ -134,17 +130,6 @@
    1.22    | string_for_failure Inappropriate =
    1.23      "The problem lies outside the prover's scope."
    1.24    | string_for_failure OutOfResources = "The prover ran out of resources."
    1.25 -  | string_for_failure SpassTooOld =
    1.26 -    "Isabelle requires a more recent version of SPASS with support for the \
    1.27 -    \TPTP syntax. To install it, download and extract the package \
    1.28 -    \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
    1.29 -    \\"spass-3.7\" directory's absolute path to " ^
    1.30 -    Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
    1.31 -    " on a line of its own."
    1.32 -  | string_for_failure VampireTooOld =
    1.33 -    "Isabelle requires a more recent version of Vampire. To install it, follow \
    1.34 -    \the instructions from the Sledgehammer manual (\"isabelle doc\
    1.35 -    \ sledgehammer\")."
    1.36    | string_for_failure NoPerl = "Perl" ^ missing_message_tail
    1.37    | string_for_failure NoLibwwwPerl =
    1.38      "The Perl module \"libwww-perl\"" ^ missing_message_tail