diff -r e7519207c2b7 -r 19106a9975c1 CookBook/Recipes/Antiquotes.thy
--- a/CookBook/Recipes/Antiquotes.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -32,7 +32,7 @@
 
 *}
 
-ML %linenumbers {*fun ml_val code_txt = "val _ = " ^ code_txt
+ML%linenumbers{*fun ml_val code_txt = "val _ = " ^ code_txt
 
 fun output_ml src ctxt code_txt =
   (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
@@ -40,8 +40,7 @@
                                             (space_explode "\n" code_txt))
 
 val _ = ThyOutput.add_commands
- [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]
-*}
+ [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]*}
 
 text {*
 
@@ -68,15 +67,14 @@
 
 *}
 
-ML %linenumbers {* fun output_ml src ctxt (code_txt,pos) =
+ML%linenumbers{*fun output_ml src 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))
 
 val _ = ThyOutput.add_commands
  [("ML_checked", ThyOutput.args 
-       (Scan.lift (OuterParse.position Args.name)) output_ml)]
-*}
+       (Scan.lift (OuterParse.position Args.name)) output_ml)] *}
 
 text {*
   where in Lines 1 and 2 the positional information is properly treated.
@@ -107,31 +105,26 @@
 
 *}
 
-ML {* 
-fun ml_pat (code_txt, pat) =
+ML{*fun ml_pat (code_txt, pat) =
    let val pat' = 
          implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
    in 
      "val " ^ pat' ^ " = " ^ code_txt 
-   end
-*}
+   end*}
 
 text {* 
   Next we like to add a response indicator to the result using:
 *}
 
 
-ML {*
-fun add_response_indicator pat =
-  map (fn s => "> " ^ s) (space_explode "\n" pat)
-*}
+ML{*fun add_response_indicator pat =
+  map (fn s => "> " ^ s) (space_explode "\n" pat) *}
 
 text {* 
   The rest of the code of the antiquotation is
   *}
 
-ML {*
-fun output_ml_response src ctxt ((code_txt,pat),pos) = 
+ML{*fun output_ml_response src 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_response_indicator pat)
@@ -143,8 +136,7 @@
  [("ML_response", 
      ThyOutput.args 
       (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
-        output_ml_response)]
-*}
+        output_ml_response)]*}
 
 text {*
   This extended antiquotation allows us to write