--- 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
*}