diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Misc/Option2.thy
--- a/doc-src/TutorialI/Misc/Option2.thy	Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy	Sat May 19 12:19:23 2001 +0200
@@ -11,7 +11,7 @@
 datatype 'a option = None | Some 'a;
 
 text{*\noindent
-Frequently one needs to add a distiguished element to some existing type.
+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
 some value @{term v} (represented by @{term"Some v"}).