diff -r b87b41ade3b2 -r deae80045527 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jan 10 01:13:41 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Jan 10 11:22:03 2002 +0100
@@ -128,7 +128,7 @@
 
   Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
   role, it may fail to prove a valid formula, for example
-  \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. Fortunately, such examples are rare.
+  \isa{m{\isacharplus}m\ {\isasymnoteq}\ n{\isacharplus}n{\isacharplus}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}. Fortunately, such examples are rare.
 \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%