# HG changeset patch
# User wenzelm
# Date 1392567446 -3600
# Node ID 0e161deca64db3890980cedb2d4b5f47773dd557
# Parent  8ef781e282d97972774d222109ba5b416b787cd0
more markup;

diff -r 8ef781e282d9 -r 0e161deca64d src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sun Feb 16 16:48:30 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Sun Feb 16 17:17:26 2014 +0100
@@ -86,17 +86,24 @@
 val and_ = Args.$$$ "and";
 val by = Args.$$$ "by";
 val goal = Scan.unless (by || and_) Args.name_inner_syntax;
+val goals1 = Scan.repeat1 goal;
 
 val _ = Theory.setup
   (ML_Context.add_antiq (Binding.name "lemma")
     (Scan.depend (fn context =>
-      Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
-      (by |-- Method.parse -- Scan.option Method.parse) >>
-        (fn ((is_open, raw_propss), methods) =>
+      Args.mode "open" -- goals1 -- Scan.repeat (Parse.position and_ -- Parse.!!! goals1) --
+      (Parse.position by -- (Method.parse -- Scan.option Method.parse)) >>
+        (fn (((is_open, raw_props), and_propss), ((_, by_pos), methods)) =>
           let
             val ctxt = Context.proof_of context;
 
-            val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
+            val reports =
+              (by_pos, Markup.keyword1) ::
+                map (fn ((_, and_pos), _) => (and_pos, Markup.keyword2)) and_propss;
+            val _ = Context_Position.reports ctxt reports;
+
+            val propss =
+              burrow (map (rpair []) o Syntax.read_props ctxt) (raw_props :: map #2 and_propss);
             val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
             fun after_qed res goal_ctxt =
               Proof_Context.put_thms false (Auto_Bind.thisN,