diff -r 8648c6651f07 -r d4866f6ff2f9 doc-src/Tutorial/tutorial.ind
--- a/doc-src/Tutorial/tutorial.ind	Tue Jan 12 15:40:53 1999 +0100
+++ b/doc-src/Tutorial/tutorial.ind	Tue Jan 12 15:48:59 1999 +0100
@@ -91,6 +91,11 @@
   \indexspace
 
   \item {\tt nat}, 2, \bold{16}
+  \item {\tt None}, \bold{32}
+
+  \indexspace
+
+  \item {\tt option}, \bold{32}
 
   \indexspace
 
@@ -114,6 +119,7 @@
   \item {\tt simp_tac}, \bold{21}
   \item simplifier, \bold{19}
   \item simpset, \bold{20}
+  \item {\tt Some}, \bold{32}
 
   \indexspace