--- 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;