# HG changeset patch
# User blanchet
# Date 1291843073 -3600
# Node ID 1b796ffa83473fa18f03cb9617ad0b75897fbee3
# Parent  0afdf5cde8743541ccdeb4bc270a3017eb5efdc4
reword error message

diff -r 0afdf5cde874 -r 1b796ffa8347 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 08 22:17:53 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 08 22:17:53 2010 +0100
@@ -109,7 +109,8 @@
   | string_for_failure prover InternalError =
     "An internal " ^ prover ^ " error occurred."
   | string_for_failure prover UnknownError =
-    "An unknown " ^ prover ^ " error occurred."
+    (* "An" is correct for "ATP" and "SMT". *)
+    "An " ^ prover ^ " error occurred."
 
 fun extract_delimited (begin_delim, end_delim) output =
   output |> first_field begin_delim |> the |> snd