diff -r 93d5408eb7d9 -r fbd097aec213 doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Sun Oct 21 19:48:19 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Sun Oct 21 19:49:29 2001 +0200
@@ -1,6 +1,7 @@
 %
 \begin{isabellebody}%
 \def\isabellecontext{Nested{\isadigit{1}}}%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -13,9 +14,11 @@
 simplifies matters because we are now free to use the recursion equation
 suggested at the end of \S\ref{sec:nested-datatype}:%
 \end{isamarkuptext}%
+\isamarkuptrue%
 \isacommand{recdef}\ trev\ {\isachardoublequote}measure\ size{\isachardoublequote}\isanewline
 \ {\isachardoublequote}trev\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ Var\ x{\isachardoublequote}\isanewline
-\ {\isachardoublequote}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}rev{\isacharparenleft}map\ trev\ ts{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\ {\isachardoublequote}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}rev{\isacharparenleft}map\ trev\ ts{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
 \begin{isamarkuptext}%
 \noindent
 Remember that function \isa{size} is defined for each \isacommand{datatype}.
@@ -37,6 +40,8 @@
 continue with our definition.  Below we return to the question of how
 \isacommand{recdef} knows about \isa{map}.%
 \end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex