diff -r 332347b9b942 -r 30da2f5eaf57 doc-src/TutorialI/Recdef/termination.thy
--- a/doc-src/TutorialI/Recdef/termination.thy	Tue Jul 17 13:46:21 2001 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Tue Jul 17 15:07:36 2001 +0200
@@ -41,8 +41,9 @@
 
 text{*\noindent
 Because \isacommand{recdef}'s termination prover involves simplification,
-we include with our second attempt the hint to use @{thm[source]termi_lem} as
-a simplification rule:\indexbold{*recdef_simp}
+we include in our second attempt a hint: the \attrdx{recdef_simp} attribute 
+says to use @{thm[source]termi_lem} as
+a simplification rule.  
 *}
 
 consts g :: "nat\<times>nat \<Rightarrow> nat";