diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Misc/Option2.thy
--- a/doc-src/TutorialI/Misc/Option2.thy	Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy	Mon May 02 11:03:27 2005 +0200
@@ -14,7 +14,7 @@
 text{*\noindent
 Frequently one needs to add a distinguished element to some existing type.
 For example, type @{text"t option"} can model the result of a computation that
-may either terminate with an error (represented by @{term None}) or return
+may either terminate with an error (represented by @{const None}) or return
 some value @{term v} (represented by @{term"Some v"}).
 Similarly, @{typ nat} extended with $\infty$ can be modeled by type
 @{typ"nat option"}. In both cases one could define a new datatype with