got rid of old error -- users who install SPASS manually are responsible for any version mismatches
--- 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
--- 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"),