diff -r 3f617d7a2691 -r 890fbfef6d6b CookBook/chunks.ML
--- a/CookBook/chunks.ML	Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/chunks.ML	Wed Mar 11 01:43:28 2009 +0000
@@ -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;