diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Misc/Option2.thy
--- a/doc-src/TutorialI/Misc/Option2.thy	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy	Tue Jul 17 13:46:21 2001 +0200
@@ -4,7 +4,8 @@
 hide type option
 (*>*)
 
-text{*\indexbold{*option}\indexbold{*None}\indexbold{*Some}
+text{*\indexbold{*option (type)}\indexbold{*None (constant)}%
+\indexbold{*Some (constant)}
 Our final datatype is very simple but still eminently useful:
 *}