--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Aug 28 16:58:27 2014 +0200
@@ -193,7 +193,7 @@
". This could be due to inconsistent axioms (including \"sorry\"s) or to \
\a bug in Sledgehammer. If the problem persists, please contact the \
\Isabelle developers."
- | string_of_atp_failure CantConnect = "Cannot connect to remote server."
+ | string_of_atp_failure CantConnect = "Cannot connect to server."
| string_of_atp_failure TimedOut = "Timed out."
| string_of_atp_failure Inappropriate =
"The generated problem lies outside the prover's scope."