doc-src/Sledgehammer/sledgehammer.tex

 Sledgehammer tries to give informative error messages. Please report any strange
 error to \authoremail. This applies double if you get the message
 
 \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?}
 
 Problems can be easy for \textit{auto} and difficult for automatic provers, but