# HG changeset patch
# User wenzelm
# Date 1393321812 -3600
# Node ID d8270c17b5beffb0eb9e88690156893139c04420
# Parent  97ff9276e12db43c26f8d58b77f70304e42cba52
more markup;

diff -r 97ff9276e12d -r d8270c17b5be src/Pure/Thy/thy_output.ML
--- 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 *)