diff -r 04cc6b4b3439 -r 50eab0183aea doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Jun 16 18:25:54 2005 +0200
@@ -640,6 +640,7 @@
 which makes Isabelle show the cause of unification failures (in Proof
 General's \textsf{Trace} buffer).
 \end{pgnote}
+\noindent
 For example, suppose we are trying to prove this subgoal by assumption:
 \begin{isabelle}
 \ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
@@ -648,10 +649,9 @@
 \begin{isabelle}
 \isacommand{apply} assumption
 \end{isabelle}
-Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information that \isa{e} clashes with \isa{c}:
+In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}:
 \begin{isabelle}
-Clash: e =/= c\isanewline
-Clash: == =/= Trueprop
+Clash: e =/= c
 \end{isabelle}
 
 Isabelle uses