diff -r fe13743ffc8b -r 3370f6aa3200 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Mon Sep 11 18:00:47 2000 +0200
@@ -1,14 +1,13 @@
 %
 \begin{isabellebody}%
+\def\isabellecontext{natsum}%
 %
 \begin{isamarkuptext}%
 \noindent
 In particular, there are \isa{case}-expressions, for example
-%
 \begin{isabelle}%
 \ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
-\end{isabelle}%
-
+\end{isabelle}
 primitive recursion, for example%
 \end{isamarkuptext}%
 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline