diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/Recipes/Antiquotes.thy
--- a/CookBook/Recipes/Antiquotes.thy	Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Wed Mar 11 01:43:28 2009 +0000
@@ -36,15 +36,15 @@
 
 *}
 
+ML {* Pretty.str *}
+
 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
 
-fun output_ml src ctxt code_txt =
+fun output_ml {source = src, context = ctxt, ...} code_txt =
   (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
-  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
-                                            (space_explode "\n" code_txt))
+  ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
-val _ = ThyOutput.add_commands
- [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]*}
+val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
 
 text {*
 
@@ -53,13 +53,13 @@
   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_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the
+  "ThyOutput.output"} in the next line pretty prints the
   code. This function expects that the code is a list of 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 for antiquotations
-  that are observed by @{ML ThyOutput.output_list} when printing the code (including
-  @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}).
+  which produces this list according to linebreaks.  There are a number of options 
+  for antiquotations that are observed by @{ML ThyOutput.output} when printing the 
+  code (including @{text "[display]"} and @{text "[quotes]"}).
 
   \begin{readmore}
   For more information about options of antiquotations see \rsccite{sec:antiq}).
@@ -70,14 +70,12 @@
   can improve the code above slightly by writing 
 *}
 
-ML%linenosgray{*fun output_ml src ctxt (code_txt,pos) =
+ML%linenosgray{*fun output_ml {source = src, context = ctxt, ...} (code_txt,pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
-  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
-                                            (space_explode "\n" code_txt))
+  ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
-val _ = ThyOutput.add_commands
- [("ML_checked", ThyOutput.args 
-       (Scan.lift (OuterParse.position Args.name)) output_ml)] *}
+val _ = ThyOutput.antiquotation "ML_checked"
+       (Scan.lift (OuterParse.position Args.name)) output_ml *}
 
 text {*
   where in Lines 1 and 2 the positional information is properly treated.
@@ -129,19 +127,16 @@
   The rest of the code of the antiquotation is
 *}
 
-ML{*fun output_ml_resp src ctxt ((code_txt,pat),pos) = 
+ML{*fun output_ml_resp {source = src, context = ctxt, ...} ((code_txt,pat),pos) = 
   (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat));
    let 
      val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat)
    in 
-     ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output 
+     ThyOutput.output (map Pretty.str output) 
    end)
 
-val _ = ThyOutput.add_commands
- [("ML_resp", 
-     ThyOutput.args 
-      (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
-        output_ml_resp)]*}
+val _ = ThyOutput.antiquotation "ML_resp" 
+     (Scan.lift (OuterParse.position (Args.name -- Args.name))) output_ml_resp*}
 
 text {*
   This extended antiquotation allows us to write