diff -r c452fea3ce74 -r 499637e8f2c6 doc-src/TutorialI/Recdef/Nested1.thy
--- a/doc-src/TutorialI/Recdef/Nested1.thy	Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Wed Oct 11 09:09:06 2000 +0200
@@ -1,7 +1,6 @@
 (*<*)
 theory Nested1 = Nested0:;
 (*>*)
-consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term";
 
 text{*\noindent
 Although the definition of @{term trev} is quite natural, we will have