diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/document/Nested0.tex
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Aug 30 18:09:20 2000 +0200
@@ -13,9 +13,7 @@
 you needed to reprove many lemmas reminiscent of similar lemmas about
 \isa{rev}. We will now show you how \isacommand{recdef} can simplify
 definitions and proofs about nested recursive datatypes. As an example we
-chose exercise~\ref{ex:trev-trev}:
-
-FIXME: declare trev now!%
+choose exercise~\ref{ex:trev-trev}:%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables: