diff -r ca8cd110f769 -r 2d6782e71702 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Tue May 07 14:28:34 2002 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Tue May 07 15:03:50 2002 +0200
@@ -107,7 +107,7 @@
 text{*\noindent
 
 Armed with this lemma, we use the \attrdx{recdef_wf} attribute to attach a
-crucial hint to our definition:
+crucial hint\cmmdx{hints} to our definition:
 *}
 (*<*)
 consts g :: "nat \<Rightarrow> nat"