--- 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: