src/Pure/Thy/thy_output.ML

--- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 15:30:29 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 16:30:07 2014 +0100
@@ -92,11 +92,8 @@
 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
 
 fun command src state ctxt =
-  let
-    val ((xname, _), pos) = Args.dest_src src;
-    val (name, f) =
-      Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) (xname, pos);
-  in f src state ctxt end;
+  let val (src', f) = Args.check_src (Context.Proof ctxt) (#1 (get_antiquotations ctxt)) src
+  in f src' state ctxt end;
 
 fun option ((xname, pos), s) ctxt =
   let
@@ -155,7 +152,7 @@
 val antiq =
   Parse.!!!
     (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof)
-  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
+  >> (fn ((name, props), args) => (props, Args.src name args));
 
 end;
 
@@ -615,12 +612,11 @@
 
 val _ = Theory.setup
   (antiquotation (Binding.name "lemma")
-    (Args.prop --
+    (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
       Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
-    (fn {source, context = ctxt, ...} => fn (prop, (((_, by_pos), m1), m2)) =>
+    (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
       let
-        val prop_src =
-          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
+        val prop_src = Args.src (Args.name_of_src source) [prop_token];
 
         val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
         val _ = Context_Position.reports ctxt reports;