# HG changeset patch
# User blanchet
# Date 1409237907 -7200
# Node ID 42e998248ddc53da35192188e01a75b117d0b0bf
# Parent  df0d6ce8fb66ad5f629ba0a863a60f051b102603
tuned message

diff -r df0d6ce8fb66 -r 42e998248ddc src/HOL/Tools/ATP/atp_proof.ML
--- 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."