# HG changeset patch
# User blanchet
# Date 1377708290 -7200
# Node ID 16235bb41881acea808e8234eff23daff634d4b7
# Parent  f13c49dd98053ada52a2427211c864d557938a6e
got rid of old error -- users who install SPASS manually are responsible for any version mismatches

diff -r f13c49dd9805 -r 16235bb41881 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 28 18:44:50 2013 +0200
@@ -25,7 +25,6 @@
     TimedOut |
     Inappropriate |
     OutOfResources |
-    OldSPASS |
     NoPerl |
     NoLibwwwPerl |
     MalformedInput |
@@ -81,7 +80,6 @@
   TimedOut |
   Inappropriate |
   OutOfResources |
-  OldSPASS |
   NoPerl |
   NoLibwwwPerl |
   MalformedInput |
@@ -125,15 +123,6 @@
   | string_of_failure Inappropriate =
     "The generated problem lies outside the prover's scope."
   | string_of_failure OutOfResources = "The prover ran out of resources."
-  | string_of_failure OldSPASS =
-    "The version of SPASS you are using is obsolete. Please upgrade to \
-    \SPASS 3.8ds. To install it, download and extract the package \
-    \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \
-    \\"spass-3.8ds\" directory's absolute path to " ^
-    quote (Path.implode (Path.expand (Path.appends
-               (Path.variable "ISABELLE_HOME_USER" ::
-                map Path.basic ["etc", "components"])))) ^
-    " on a line of its own."
   | string_of_failure NoPerl = "Perl" ^ missing_message_tail
   | string_of_failure NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
diff -r f13c49dd9805 -r 16235bb41881 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 28 18:44:50 2013 +0200
@@ -529,8 +529,7 @@
        |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
-     [(OldSPASS, "Unrecognized option Isabelle"),
-      (GaveUp, "SPASS beiseite: Completion found"),
+     [(GaveUp, "SPASS beiseite: Completion found"),
       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),