delimiter markup for verbatim tokens;

--- a/src/Pure/Thy/latex.ML	Mon Aug 29 16:18:06 2005 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Aug 29 16:18:07 2005 +0200
@@ -108,7 +108,8 @@
       enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
     else if T.is_kind T.AltString tok then
       enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
-    else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
+    else if T.is_kind T.Verbatim tok then
+      enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" (output_syms s)
     else output_syms s
   end;