clarified syntax -- avoid overlap with command category;

--- a/src/Pure/ML/ml_thms.ML	Sat Nov 01 19:47:48 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Sat Nov 01 20:19:07 2014 +0100
@@ -80,16 +80,17 @@
 (* ad-hoc goals *)
 
 val and_ = Args.$$$ "and";
-val by = Args.$$$ "by";
+val by = Parse.reserved "by";
 val goal = Scan.unless (by || and_) Args.name_inner_syntax;
 
 val _ = Theory.setup
   (ML_Antiquotation.declaration @{binding lemma}
     (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
-      (by |-- Method.parse -- Scan.option Method.parse)))
-    (fn _ => fn ((is_open, raw_propss), (m1, m2)) => fn ctxt =>
+      (Parse.position by -- Method.parse -- Scan.option Method.parse)))
+    (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
       let
-        val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
+        val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2);
+        val _ = Context_Position.reports ctxt reports;
 
         val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
         val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;

--- a/src/Pure/Thy/thy_output.ML	Sat Nov 01 19:47:48 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Nov 01 20:19:07 2014 +0100
@@ -615,12 +615,10 @@
 
 (* embedded lemma *)
 
-val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
-
 val _ = Theory.setup
   (antiquotation @{binding lemma}
     (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
-      Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
+      Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
     (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
       let
         val prop_src = Token.src (Token.name_of_src source) [prop_token];