diff -r 47ff45771f2c -r 185110a4b97a doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Mon Nov 10 08:18:58 2008 +0100
+++ b/doc-src/more_antiquote.ML	Mon Nov 10 09:03:28 2008 +0100
@@ -7,7 +7,7 @@
 
 signature MORE_ANTIQUOTE =
 sig
-  val verbatim: string -> string
+  val typewriter: string -> string
 end;
 
 structure More_Antiquote : MORE_ANTIQUOTE =
@@ -15,9 +15,9 @@
 
 structure O = ThyOutput;
 
-(* printing verbatim lines *)
+(* printing typewriter lines *)
 
-fun verbatim s =
+fun typewriter s =
   let
     val parse = Scan.repeat
       (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
@@ -43,7 +43,7 @@
     val (texts, []) =  Scan.finite Symbol.stopper parse cs
   in if null texts
     then ""
-    else implode ("\\isaverbatim%\n\\noindent%\n\\hspace*{0pt}" :: texts)
+    else implode ("\\isatypewriter%\n\\noindent%\n\\hspace*{0pt}" :: texts)
   end
 
 
@@ -91,7 +91,7 @@
     Code_Target.code_of (ProofContext.theory_of ctxt)
       target "Example" (mk_cs (ProofContext.theory_of ctxt))
         (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
-    |> verbatim;
+    |> typewriter;
 
 in