diff -r f718767efd49 -r f8a734dc0fbc doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Wed Jun 22 07:54:13 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jun 22 09:26:18 2005 +0200
@@ -635,10 +635,10 @@
 filled in later, sometimes in stages and often automatically. 
 
 \begin{pgnote}
-If unification fails when you think it should succeed, try setting the Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
-\textsf{Trace Unification},
+If unification fails when you think it should succeed, try setting the Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
+\pgmenu{Trace Unification},
 which makes Isabelle show the cause of unification failures (in Proof
-General's \textsf{Trace} buffer).
+General's \pgmenu{Trace} buffer).
 \end{pgnote}
 \noindent
 For example, suppose we are trying to prove this subgoal by assumption: