--- a/doc-src/TutorialI/Misc/document/Option2.tex Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Misc/document/Option2.tex Mon Nov 08 00:00:47 2010 +0100
@@ -22,7 +22,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
-\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%
+\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{3D}{\isacharequal}}\ None\ {\isaliteral{7C}{\isacharbar}}\ Some\ {\isaliteral{27}{\isacharprime}}a%
\begin{isamarkuptext}%
\noindent
Frequently one needs to add a distinguished element to some existing type.