diff -r 1cc848548f21 -r e92f2e44e4d8 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Mar 14 20:29:26 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Mar 14 21:02:34 2021 +0100
@@ -25,12 +25,9 @@
     ProofIncomplete |
     ProofUnparsable |
     UnsoundProof of bool * string list |
-    CantConnect |
     TimedOut |
     Inappropriate |
     OutOfResources |
-    NoPerl |
-    NoLibwwwPerl |
     MalformedInput |
     MalformedOutput |
     Interrupted |
@@ -139,12 +136,9 @@
   ProofIncomplete |
   ProofUnparsable |
   UnsoundProof of bool * string list |
-  CantConnect |
   TimedOut |
   Inappropriate |
   OutOfResources |
-  NoPerl |
-  NoLibwwwPerl |
   MalformedInput |
   MalformedOutput |
   Interrupted |
@@ -180,14 +174,10 @@
   | string_of_atp_failure (UnsoundProof (true, ss)) =
     "The prover derived \"False\"" ^ from_lemmas ss ^
     ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
-  | 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
-  | string_of_atp_failure NoLibwwwPerl =
-    "The Perl module \"libwww-perl\"" ^ missing_message_tail
   | string_of_atp_failure MalformedInput = "The generated problem is malformed"
   | string_of_atp_failure MalformedOutput = "The prover output is malformed"
   | string_of_atp_failure Interrupted = "The prover was interrupted"