diff -r 624279d187e1 -r b02904872d6b CookBook/Readme.thy
--- a/CookBook/Readme.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Readme.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -143,12 +143,12 @@
 
 
   \item Functions and value bindings cannot be defined inside antiquotations; they need
-  to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
+  to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
   environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 
   the Cookbook, however, ensures that the environment markers are not printed.
 
   \item Line numbers can be printed using 
-  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 
+  \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"}
   for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs.
 
   \end{itemize}