--- a/CookBook/Parsing.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Parsing.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -597,7 +597,7 @@
   \isacommand{theory}~@{text Command}\\
   \isacommand{imports}~@{text Main}\\
   \isacommand{begin}\\
-  \isacommand{ML}~\isa{\isacharverbatimopen}\\
+  \isacommand{ML}~@{text "\<verbopen>"}\\
   @{ML
 "let
   val do_nothing = Scan.succeed (Toplevel.theory I)
@@ -605,7 +605,7 @@
 in
   OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
-  \isa{\isacharverbatimclose}\\
+  @{text "\<verbclose>"}\\
   \isacommand{end}
   \end{graybox}
   \caption{\small The file @{text "Command.thy"} is necessary for generating a log