diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
 %
 \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
@@ -20,11 +21,9 @@
 Remember that function \isa{size} is defined for each \isacommand{datatype}.
 However, the definition does not succeed. Isabelle complains about an
 unproved termination condition
-%
 \begin{isabelle}%
 \ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
-\end{isabelle}%
-
+\end{isabelle}
 where \isa{set} returns the set of elements of a list (no special
 knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
 (when \isa{term} was defined).  First we have to understand why the