diff -r d3fcc1a0272c -r 90bee31628dc CookBook/chunks.ML
--- a/CookBook/chunks.ML	Thu Feb 26 13:46:05 2009 +0100
+++ b/CookBook/chunks.ML	Thu Mar 12 08:11:02 2009 +0100
@@ -139,7 +139,7 @@
      || Scan.one not_eof >> ML_Lex.content_of)) #>
   fst;
 
-fun output_chunk src ctxt name =
+fun output_chunk {state: Toplevel.state, source = src, context = ctxt} name =
   let
     val toks = the_chunk (ProofContext.theory_of ctxt) name;
     val (spc, toks') = (case toks of
@@ -164,7 +164,6 @@
     output_list (fn _ => fn s => Pretty.str s) src ctxt
   end;
 
-val _ = ThyOutput.add_commands
-  [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)];
+val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;
 
 end;