doc-src/Classes/Thy/Classes.thy

--- a/doc-src/Classes/Thy/Classes.thy	Fri Sep 24 14:03:44 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Fri Sep 24 14:56:16 2010 +0200
@@ -601,19 +601,15 @@
   \noindent This maps to Haskell as follows:
 *}
 (*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts example (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts example (Haskell)}
 *}
 
 text {*
   \noindent The code in SML has explicit dictionary passing:
 *}
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts example (SML)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts example (SML)}
 *}
 
 
@@ -621,10 +617,8 @@
   \noindent In Scala, implicts are used as dictionaries:
 *}
 (*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts example (Scala)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts example (Scala)}
 *}