--- a/doc-src/TutorialI/fp.tex Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/fp.tex Mon Aug 21 19:17:07 2000 +0200
@@ -862,4 +862,4 @@
\label{sec:advanced-ind}
\input{Misc/document/AdvancedInd.tex}
-\input{Datatype/document/Nested2.tex}
+%\input{Datatype/document/Nested2.tex}