doc-src/Codegen/Thy/Introduction.thy

--- a/doc-src/Codegen/Thy/Introduction.thy	Mon Sep 27 16:19:37 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy	Mon Sep 27 16:27:31 2010 +0200
@@ -70,7 +70,7 @@
 
 text {* \noindent resulting in the following code: *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts empty enqueue dequeue (SML)}
 *}
 
@@ -93,7 +93,7 @@
   \noindent This is the corresponding code:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts empty enqueue dequeue (Haskell)}
 *}
 
@@ -168,7 +168,7 @@
   native classes:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts bexp (Haskell)}
 *}
 
@@ -178,7 +178,7 @@
   @{text SML}:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{code_stmts bexp (SML)}
 *}