
diff -r e336ef6313aa -r d7447b8c4265 doc-src/Sledgehammer/sledgehammer.tex
--- 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?}




