--- 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?}
--- 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 =