--- a/CookBook/antiquote_setup.ML	Fri Nov 28 05:56:28 2008 +0100
+++ b/CookBook/antiquote_setup.ML	Sat Nov 29 21:20:18 2008 +0000
@@ -22,12 +22,12 @@
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
 
-fun output_ml_open ml src ctxt ((txt,ovars),pos) =
+fun output_ml ml src ctxt ((txt,ovars),pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);
   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))
 
-fun output_ml ml src ctxt (txt,pos) =
-  output_ml_open (K ml) src ctxt ((txt,()),pos) 
+fun output_ml_aux ml src ctxt (txt,pos) =
+  output_ml (K ml) src ctxt ((txt,()),pos) 
 
 fun add_response_indicator txt =
   map (fn s => "> " ^ s) (space_explode "\n" txt)
@@ -48,19 +48,19 @@
   else error ("Source file " ^ quote txt ^ " does not exist.")
 
 val _ = ThyOutput.add_commands
-  [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
+  [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
       (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-       Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_open ml_val_open)),
+       Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) 
+                                                                 (output_ml ml_val_open)),
    ("ML_file", ThyOutput.args (Scan.lift Args.name)
       (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))),
    ("ML_text", ThyOutput.args (Scan.lift Args.name)
       (ThyOutput.output (fn _ => fn s => Pretty.str s))),
-   ("ML", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val)),
    ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       (output_ml_response ml_pat)),
    ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       (output_ml_response_fake ml_val)),
-   ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_struct)),
-   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_type))];
+   ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),
+   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))];
    
 end;