diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -2,7 +2,7 @@
 theory natsum = Main:;
 (*>*)
 text{*\noindent
-In particular, there are \isa{case}-expressions, for example
+In particular, there are @{text"case"}-expressions, for example
 \begin{quote}
 @{term[display]"case n of 0 => 0 | Suc m => m"}
 \end{quote}