diff -r c452fea3ce74 -r 499637e8f2c6 doc-src/TutorialI/Recdef/document/Nested0.tex
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Oct 11 09:09:06 2000 +0200
@@ -16,7 +16,7 @@
 definitions and proofs about nested recursive datatypes. As an example we
 choose exercise~\ref{ex:trev-trev}:%
 \end{isamarkuptext}%
-\end{isabellebody}%
+\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"