diff -r 066e2d4d0de8 -r f75a01ee6c41 doc-src/Codegen/Thy/Introduction.thy
--- a/doc-src/Codegen/Thy/Introduction.thy	Fri Sep 24 15:11:38 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Fri Sep 24 15:11:38 2010 +0200
@@ -70,10 +70,8 @@
 
 text {* \noindent resulting in the following code: *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts empty enqueue dequeue (SML)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts empty enqueue dequeue (SML)}
 *}
 
 text {*
@@ -95,10 +93,8 @@
   \noindent This is the corresponding code:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts empty enqueue dequeue (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts empty enqueue dequeue (Haskell)}
 *}
 
 text {*
@@ -172,10 +168,8 @@
   native classes:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts bexp (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts bexp (Haskell)}
 *}
 
 text {*
@@ -184,10 +178,8 @@
   @{text SML}:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts bexp (SML)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts bexp (SML)}
 *}
 
 text {*