# HG changeset patch
# User blanchet
# Date 1280426522 -7200
# Node ID 488b38cd3e0627641492d4b66b15bd46f5573bfb
# Parent  7627881fe9d4104d19fc89d135fe1126665ac113
avoid "ATP Error: Error: blah" style messages

diff -r 7627881fe9d4 -r 488b38cd3e06 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 19:58:43 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jul 29 20:02:02 2010 +0200
@@ -64,10 +64,10 @@
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "The ATP ran out of resources."
   | string_for_failure OldSpass =
-    "Warning: Isabelle requires a more recent version of SPASS with \
-    \support for the TPTP syntax. To install it, download and extract the \
-    \package \"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and \
-    \add the \"spass-3.7\" directory's absolute path to " ^
+    "Isabelle requires a more recent version of SPASS with support for the \
+    \TPTP syntax. To install it, download and extract the package \
+    \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
+    \\"spass-3.7\" directory's absolute path to " ^
     quote (Path.implode (Path.expand (Path.appends
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
@@ -76,10 +76,10 @@
   | string_for_failure NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
   | string_for_failure MalformedInput =
-    "Internal Isabelle error: The ATP problem is malformed. Please report \
-    \this to the Isabelle developers."
-  | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
-  | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
+    "The ATP problem is malformed. Please report this to the Isabelle \
+    \developers."
+  | string_for_failure MalformedOutput = "The ATP output is malformed."
+  | string_for_failure UnknownError = "An unknown ATP error occurred."
 
 fun known_failure_in_output output =
   find_first (fn (_, pattern) => String.isSubstring pattern output)