diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Fri Jan 05 10:19:32 2001 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy	Fri Jan 05 13:10:37 2001 +0100
@@ -49,7 +49,7 @@
   to prove the goal (although it may take you some time to realize what has
   happened if @{text show_types} is not set).  In this particular example,
   you need to include an explicit type constraint, for example
-  @{prop"x+0 = (x::nat)"}. If there is enough contextual information this
+  @{text"x+0 = (x::nat)"}. If there is enough contextual information this
   may not be necessary: @{prop"Suc x = x"} automatically implies
   @{text"x::nat"} because @{term Suc} is not overloaded.
 \end{warn}