# HG changeset patch
# User blanchet
# Date 1626100216 -7200
# Node ID 96a05b8462f952029c8654044388dcd334d048f6
# Parent  34c8cf767fa3fdc881afcdfa86ed9c55fc0ab2c5
improved warning

diff -r 34c8cf767fa3 -r 96a05b8462f9 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 12 16:30:15 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 12 16:30:16 2021 +0200
@@ -169,10 +169,10 @@
   | string_of_atp_failure ProofUnparsable =
     "The prover claims the conjecture is a theorem but provided an unparsable proof"
   | string_of_atp_failure (UnsoundProof (false, ss)) =
-    "The prover derived \"False\"" ^ from_lemmas ss ^
+    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
     "; specify a sound type encoding or omit the \"type_enc\" option"
   | string_of_atp_failure (UnsoundProof (true, ss)) =
-    "The prover derived \"False\"" ^ from_lemmas ss ^
+    "The prover derived the lemma \"False\"" ^ from_lemmas ss ^
     ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
   | string_of_atp_failure TimedOut = "Timed out"
   | string_of_atp_failure Inappropriate =