diff -r 42671298f037 -r 313a24b66a8d doc-src/TutorialI/Misc/document/Option2.tex
--- 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.