diff -r 624279d187e1 -r b02904872d6b CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -30,11 +30,10 @@
 
 \begin{isabelle}
 \begin{graybox}
-\isa{\isacommand{ML}
-\isacharverbatimopen\isanewline
+\isacommand{ML}~@{text "\<verbopen>"}\isanewline
 \hspace{5mm}@{ML "3 + 4"}\isanewline
-\isacharverbatimclose\isanewline
-@{text "> 7"}\smallskip}
+@{text "\<verbclose>"}\isanewline
+@{text "> 7"}\smallskip
 \end{graybox}
 \end{isabelle}
 
@@ -43,7 +42,7 @@
   your Isabelle environment. The code inside the \isacommand{ML}-command 
   can also contain value and function bindings, and even those can be
   undone when the proof script is retracted. As mentioned earlier, we will  
-  drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 
+  drop the \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} 
   whenever we show code.
 
   Once a portion of code is relatively stable, one usually wants to