src/Pure/ML/ml_thms.ML
changeset 55914 c5b752d549e3
parent 55795 2d4cf0005a02
child 55997 9dc5ce83202c
--- a/src/Pure/ML/ml_thms.ML	Wed Mar 05 09:59:48 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Mar 05 13:11:08 2014 +0100
@@ -90,17 +90,13 @@
 val _ = Theory.setup
   (ML_Context.add_antiq @{binding lemma}
     (Scan.depend (fn context =>
-      Args.mode "open" -- Parse.enum1_positions "and" (Scan.repeat1 goal) --
-      Parse.position by -- Method.parse -- Scan.option Method.parse
-     >> (fn ((((is_open, (raw_propss, and_positions)), (_, by_pos)), m1), m2) =>
+      Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
+      (by |-- Method.parse -- Scan.option Method.parse)
+     >> (fn ((is_open, raw_propss), (m1, m2)) =>
           let
             val ctxt = Context.proof_of context;
 
-            val reports =
-              (by_pos, Markup.keyword1) ::
-                map (rpair Markup.keyword2) and_positions @
-                maps Method.reports_of (m1 :: the_list m2);
-            val _ = Context_Position.reports ctxt reports;
+            val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
 
             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;