diff -r 332347b9b942 -r 30da2f5eaf57 doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Tue Jul 17 13:46:21 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Tue Jul 17 15:07:36 2001 +0200
@@ -101,8 +101,8 @@
 \begin{isamarkuptext}%
 \noindent
 
-Armed with this lemma, we can append a crucial hint to our definition:
-\indexbold{*recdef_wf}%
+Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
+crucial hint to our definition:%
 \end{isamarkuptext}%
 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}%
 \begin{isamarkuptext}%