--- a/CookBook/Recipes/Antiquotes.thy	Thu Mar 12 08:11:02 2009 +0100
+++ b/CookBook/Recipes/Antiquotes.thy	Thu Mar 12 14:25:35 2009 +0000
@@ -46,13 +46,13 @@
 
 text {*
 
-  Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, 
+  The parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, 
   in this case the code. As mentioned before, the code
   is sent to the ML-compiler in the line 4 using the function @{ML ml_val},
   which constructs the appropriate ML-expression.
   If the code is ``approved'' by the compiler, then the output function @{ML
   "ThyOutput.output"} in the next line pretty prints the
-  code. This function expects that the code is a list of strings where each
+  code. This function expects that the code is a list of (pretty)strings where each
   string correspond to a line in the output. Therefore the use of 
   @{ML "(space_explode \"\\n\" txt)" for txt} 
   which produces this list according to linebreaks.  There are a number of options 
@@ -69,7 +69,7 @@
   can improve the code above slightly by writing 
 *}
 
-ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt,pos) =
+ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
    ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
@@ -77,7 +77,9 @@
          (Scan.lift (OuterParse.position Args.name)) output_ml *}
 
 text {*
-  where in Lines 1 and 2 the positional information is properly treated.
+  where in Lines 1 and 2 the positional information is properly treated. The
+  parser @{ML OuterParse.position} encodes the positional information in the 
+  result.
 
   We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to
   obtain @{ML_checked "2 + 3"} and be sure that this code compiles until