--- a/CookBook/FirstSteps.thy	Fri Oct 17 05:02:04 2008 -0400
+++ b/CookBook/FirstSteps.thy	Fri Oct 17 17:41:34 2008 -0400
@@ -5,7 +5,6 @@
 
 chapter {* First Steps *}
 
-
 text {* 
   Isabelle programming is done in Standard ML.
   Just like lemmas and proofs, code in Isabelle is part of a 
@@ -50,7 +49,7 @@
   then Isabelle's undo operation has no effect on the definition of 
   @{ML_text "foo"}. Note that from now on we will drop the 
   \isacommand{ML} @{ML_text "{"}@{ML_text "* \<dots> *"}@{ML_text "}"} whenever
-  we show code.
+  we show code and its response.
 
   Once a portion of code is relatively stable, one usually wants to 
   export it to a separate ML-file. Such files can then be included in a 
@@ -572,7 +571,7 @@
       ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");
 
 fun ml_pat (rhs, pat) =
-  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s)
+  let val pat' = implode (map (fn "\<dots>" => "_" | s => s)
     (Symbol.explode pat))
   in
     "val " ^ pat' ^ " = " ^ rhs