diff -r 4e586b734fac -r 3aa2bc9c5478 doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex	Mon Sep 27 16:27:31 2010 +0200
@@ -207,11 +207,11 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
-\isatagtypewriter
+\isatagquotetypewriter
 %
 \begin{isamarkuptext}%
 funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
@@ -224,12 +224,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
 %
-\isadelimtypewriter
+\isadelimquotetypewriter
 %
-\endisadelimtypewriter
+\endisadelimquotetypewriter
 %
 \isamarkupsubsection{Imperative data structures%
 }