diff -r c452fea3ce74 -r 499637e8f2c6 doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Wed Oct 11 09:09:06 2000 +0200
@@ -1,6 +1,5 @@
 (*<*)
 theory Nested2 = Nested0:;
-consts trev  :: "('a,'b)term => ('a,'b)term";
 (*>*)
 
 text{*\noindent