diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Misc/document/Option2.tex
--- a/doc-src/TutorialI/Misc/document/Option2.tex	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Option2.tex	Tue Jul 17 13:46:21 2001 +0200
@@ -3,7 +3,8 @@
 \def\isabellecontext{Option{\isadigit{2}}}%
 %
 \begin{isamarkuptext}%
-\indexbold{*option}\indexbold{*None}\indexbold{*Some}
+\indexbold{*option (type)}\indexbold{*None (constant)}%
+\indexbold{*Some (constant)}
 Our final datatype is very simple but still eminently useful:%
 \end{isamarkuptext}%
 \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%