--- a/src/Pure/Thy/thy_output.ML Mon Feb 24 23:17:55 2014 +0000
+++ b/src/Pure/Thy/thy_output.ML Tue Feb 25 10:50:12 2014 +0100
@@ -614,16 +614,18 @@
val _ = Theory.setup
(antiquotation (Binding.name "lemma")
- (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
- (fn {source, context, ...} => fn (prop, methods) =>
+ (Args.prop --
+ Scan.lift (Parse.position (Args.$$$ "by") -- (Method.parse -- Scan.option Method.parse)))
+ (fn {source, context = ctxt, ...} => fn (prop, ((_, by_pos), methods)) =>
let
val prop_src =
(case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
+ val _ = Context_Position.report ctxt by_pos Markup.keyword1;
(* FIXME check proof!? *)
- val _ = context
+ val _ = ctxt
|> Proof.theorem NONE (K I) [[(prop, [])]]
|> Proof.global_terminal_proof methods;
- in output context (maybe_pretty_source pretty_term context prop_src [prop]) end));
+ in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end));
(* ML text *)