--- 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;