doc-src/TutorialI/Recdef/Nested2.thy

--- a/doc-src/TutorialI/Recdef/Nested2.thy	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Jul 17 13:46:21 2001 +0200
@@ -77,7 +77,7 @@
 
 text{*\noindent
 or declare them globally
-by giving them the \isaindexbold{recdef_cong} attribute as in
+by giving them the \attrdx{recdef_cong} attribute as in
 *}
 
 declare map_cong[recdef_cong]