diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/Nested0.thy
--- a/doc-src/TutorialI/Recdef/Nested0.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested0.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -15,9 +15,7 @@
 you needed to reprove many lemmas reminiscent of similar lemmas about
 @{term"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}:
 *}
 (* consts trev  :: "('a,'b)term => ('a,'b)term" *)
 (*<*)