--- a/src/Pure/ML/ml_context.ML Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Mon Mar 10 16:30:07 2014 +0100
@@ -115,10 +115,8 @@
fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
fun antiquotation src ctxt =
- let
- val ((xname, _), pos) = Args.dest_src src;
- val (_, scan) = Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt) (xname, pos);
- in Args.context_syntax Markup.ML_antiquotationN scan src ctxt end;
+ let val (src', scan) = Args.check_src (Context.Proof ctxt) (get_antiqs ctxt) src
+ in Args.context_syntax Markup.ML_antiquotationN scan src' ctxt end;
(* parsing and evaluation *)
@@ -127,7 +125,7 @@
val antiq =
Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
- >> (fn ((x, pos), y) => Args.src ((x, y), pos));
+ >> uncurry Args.src;
val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";