diff -r 2e2a506553a3 -r af7239e3054d doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Jun 10 17:59:12 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jun 10 18:36:47 2005 +0200
@@ -634,14 +634,18 @@
 as $\exists x.\,P$, they let us proceed with a proof.  They can be 
 filled in later, sometimes in stages and often automatically. 
 
-If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{*trace_unify_fail (flag)},
-which makes Isabelle show the cause of unification failures.  For example, suppose we are trying to prove this subgoal by assumption:
+\begin{pgnote}
+If unification fails when you think it should succeed, try setting the Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
+\textsf{Trace Unification},
+which makes Isabelle show the cause of unification failures (in Proof
+General's \textsf{Trace} buffer).
+\end{pgnote}
+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)
 \end{isabelle}
 The \isa{assumption} method having failed, we try again with the flag set:
 \begin{isabelle}
-\isacommand{ML}\ "set\ trace\_unify\_fail"\isanewline
 \isacommand{apply} assumption
 \end{isabelle}
 Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information: