diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Mon Sep 27 16:27:31 2010 +0200
@@ -269,7 +269,20 @@
 %
 \isatagquote
 \isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ \ \isacommand{ML}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isadelimquotett
+\ %
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{ML}\isamarkupfalse%
 \ {\isacharverbatimopen}\isanewline
 \ \ fun\ eval{\isacharunderscore}form\ %
 \isaantiq
@@ -294,12 +307,12 @@
 \ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
 {\isacharverbatimclose}%
-\endisatagquote
-{\isafoldquote}%
+\endisatagquotett
+{\isafoldquotett}%
 %
-\isadelimquote
+\isadelimquotett
 %
-\endisadelimquote
+\endisadelimquotett
 %
 \begin{isamarkuptext}%
 \noindent \isa{code} takes as argument the name of a constant;