diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Recdef/Nested0.thy
--- a/doc-src/TutorialI/Recdef/Nested0.thy	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested0.thy	Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
 (*>*)
 
 text{*
+\index{datatypes!nested}%
 In \S\ref{sec:nested-datatype} we defined the datatype of terms
 *}