# HG changeset patch
# User blanchet
# Date 1377708290 -7200
# Node ID f13c49dd98053ada52a2427211c864d557938a6e
# Parent  79e5b668f7164d0e4245b043e87aa8fa63b2aa9b
tuned messages

diff -r 79e5b668f716 -r f13c49dd9805 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Aug 28 18:44:50 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Aug 28 18:44:50 2013 +0200
@@ -601,14 +601,15 @@
 \point{A strange error occurred---what should I do?}
 
 Sledgehammer tries to give informative error messages. Please report any strange
-error to the author at \authoremail. This applies double if you get the message
+error to the author at \authoremail. This applies doubly if you get the message
 
 \prew
 \slshape
-The prover found a type-unsound proof involving ``\textit{foo\/}'',
-``\textit{bar\/}'', and ``\textit{baz\/}'' even though a supposedly type-sound
-encoding was used (or, less likely, your axioms are inconsistent). You might
-want to report this to the Isabelle developers.
+The prover derived ``\textit{False}'' using ``\textit{foo\/}'',
+``\textit{bar\/}'', and ``\textit{baz\/}''.
+This could be due to inconsistent axioms (including ``\textbf{sorry}''s) or to
+a bug in Sledgehammer. If the problem persists, please contact the
+Isabelle developers.
 \postw
 
 \point{Auto can solve it---why not Sledgehammer?}
diff -r 79e5b668f716 -r f13c49dd9805 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 28 18:44:50 2013 +0200
@@ -103,8 +103,7 @@
 
 fun involving [] = ""
   | involving ss =
-    "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
-    " "
+    " involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
 
 fun string_of_failure Unprovable = "The generated problem is unprovable."
   | string_of_failure GaveUp = "The prover gave up."
@@ -114,13 +113,13 @@
     "The prover claims the conjecture is a theorem but provided an incomplete \
     \(or unparsable) proof."
   | string_of_failure (UnsoundProof (false, ss)) =
-    "The prover found an unsound proof " ^ involving ss ^
-    "(or, less likely, your axioms are inconsistent). Specify a sound type \
-    \encoding or omit the \"type_enc\" option."
+    "The prover derived \"False\" using" ^ involving ss ^
+    ". Specify a sound type encoding or omit the \"type_enc\" option."
   | string_of_failure (UnsoundProof (true, ss)) =
-    "The prover found an unsound proof " ^ involving ss ^
-    "(or, less likely, your axioms are inconsistent). Please report this to \
-    \the Isabelle developers."
+    "The prover derived \"False\" using" ^ involving 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_failure CantConnect = "Cannot connect to remote server."
   | string_of_failure TimedOut = "Timed out."
   | string_of_failure Inappropriate =