--- a/CookBook/Intro.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Intro.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -71,18 +71,16 @@
 
   \begin{isabelle}
   \begin{graybox}
-  \isa{\isacommand{ML}
-  \isacharverbatimopen\isanewline
+  \isacommand{ML}~@{text "\<verbopen>"}\isanewline
   \hspace{5mm}@{ML "3 + 4"}\isanewline
-  \isacharverbatimclose}
+  @{text "\<verbclose>"}
   \end{graybox}
   \end{isabelle}
   
   This corresponds to how code can be processed inside the interactive
   environment of Isabelle. It is therefore easy to experiment with the code
   (which by the way is highly recommended). However, for better readability we
-  will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots
-  \isacharverbatimclose} and just write
+  will drop the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write
 
 
   @{ML [display,gray] "3 + 4"}