diff -r c452fea3ce74 -r 499637e8f2c6 doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Wed Oct 11 09:09:06 2000 +0200
@@ -1,7 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Nested1}%
-\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
+%
 \begin{isamarkuptext}%
 \noindent
 Although the definition of \isa{trev} is quite natural, we will have