--- a/ProgTutorial/Recipes/Antiquotes.thy	Sun Aug 22 22:56:52 2010 +0800
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Sat Aug 28 13:27:16 2010 +0800
@@ -44,7 +44,7 @@
 
 fun output_ml {context = ctxt, ...} code_txt =
   (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); 
-   Thy_Output.output (map Pretty.str (space_explode "\n" code_txt)))
+   Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
 
 val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
 
@@ -75,7 +75,7 @@
 
 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =
   (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt);
-   Thy_Output.output (map Pretty.str (space_explode "\n" code_txt)))
+   Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
 
 val _ = Thy_Output.antiquotation "ML_checked"
          (Scan.lift (Parse.position Args.name)) output_ml *}
@@ -133,7 +133,7 @@
      val code_output = space_explode "\n" code_txt 
      val resp_output = add_resp (space_explode "\n" pat)
    in 
-     Thy_Output.output (map Pretty.str (code_output @ resp_output)) 
+     Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) 
    end)
 
 val _ = Thy_Output.antiquotation "ML_resp"