--- a/src/Pure/Thy/thy_output.ML Mon Mar 10 17:52:30 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Mon Mar 10 18:06:23 2014 +0100
@@ -92,7 +92,7 @@
fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
fun command src state ctxt =
- let val (src', f) = Args.check_src (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) src
+ let val (src', f) = Args.check_src ctxt (#1 (get_antiquotations ctxt)) src
in f src' state ctxt end;
fun option ((xname, pos), s) ctxt =
@@ -115,7 +115,7 @@
fun antiquotation name scan out =
add_command name
(fn src => fn state => fn ctxt =>
- let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt
+ let val (x, ctxt') = Args.syntax scan src ctxt
in out {source = src, state = state, context = ctxt'} x end);