src/HOL/Tools/ATP/atp_proof.ML

   | string_of_atp_failure (UnsoundProof (true, ss)) =
     "The prover derived \"False\"" ^ from_lemmas ss ^
     ". 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."
   | string_of_atp_failure OutOfResources = "The prover ran out of resources."
   | string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail