--- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 20 12:47:58 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 20 12:47:58 2011 +0200
@@ -439,9 +439,10 @@
\begin{quote}
\slshape
-The prover found a type-unsound proof even though a supposedly type-sound
-encoding was used (or, very unlikely, your axioms are inconsistent). You
-might want to report this to the Isabelle developers.
+The prover found a type-unsound proof involving ``\textit{foo}'',
+``\textit{bar}'', ``\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.
\end{quote}
\point{Auto can solve it---why not Sledgehammer?}