# HG changeset patch
# User wenzelm
# Date 1635419628 -7200
# Node ID 3da2662a35cdd1d3e046a877040e63dbfbd5644d
# Parent  c22ae7b41bb868b9d42f92c41d4c9c202aef141d
local fixes for "lemma" antiquotation;

diff -r c22ae7b41bb8 -r 3da2662a35cd NEWS
--- a/NEWS	Thu Oct 28 12:25:47 2021 +0200
+++ b/NEWS	Thu Oct 28 13:13:48 2021 +0200
@@ -292,6 +292,11 @@
 
 *** ML ***
 
+* Antiquotation for embedded lemma supports local fixes, as usual in
+many other Isar language elements. For example:
+
+  @{lemma "x = x" for x :: nat by (rule refl)}
+
 * Term operations under abstractions are now more robust (and more
 strict) by using the formal proof context in subsequent operations:
 
diff -r c22ae7b41bb8 -r 3da2662a35cd src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Thu Oct 28 12:25:47 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy	Thu Oct 28 13:13:48 2021 +0200
@@ -704,7 +704,7 @@
   @@{ML_antiquotation thms} thms
   ;
   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
-    @'by' method method?
+    @{syntax for_fixes} @'by' method method?
   ;
   @@{ML_antiquotation oracle_name} embedded
   \<close>
diff -r c22ae7b41bb8 -r 3da2662a35cd src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Thu Oct 28 12:25:47 2021 +0200
+++ b/src/Pure/ML/ml_thms.ML	Thu Oct 28 13:13:48 2021 +0200
@@ -77,23 +77,26 @@
 (* embedded lemma *)
 
 val embedded_lemma =
-  Args.mode "open" -- Parse.and_list1 (Scan.repeat1 Parse.embedded_inner_syntax) -- Method.parse_by
-    >> (fn ((is_open, raw_stmt), (methods, reports)) => fn ctxt =>
+  Args.mode "open" -- Parse.and_list1 (Scan.repeat1 Parse.embedded_inner_syntax)
+    -- Parse.for_fixes -- Method.parse_by
+    >> (fn (((is_open, raw_stmt), fixes), (methods, reports)) => fn ctxt =>
         let
           val _ = Context_Position.reports ctxt reports;
 
-          val stmt = burrow (map (rpair []) o Syntax.read_props ctxt) raw_stmt;
+          val stmt_ctxt = #2 (Proof_Context.add_fixes_cmd fixes ctxt);
+          val stmt = burrow (map (rpair []) o Syntax.read_props stmt_ctxt) raw_stmt;
+
           val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>;
           fun after_qed res goal_ctxt =
             Proof_Context.put_thms false (Auto_Bind.thisN,
               SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
 
-          val ctxt' = ctxt
+          val thms_ctxt = stmt_ctxt
             |> Proof.theorem NONE after_qed stmt
             |> Proof.global_terminal_proof methods;
           val thms =
-            Proof_Context.get_fact ctxt'
-              (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)))
+            Proof_Context.get_fact thms_ctxt
+              (Facts.named (Proof_Context.full_name thms_ctxt (Binding.name Auto_Bind.thisN)))
         in thms end);
 
 val _ = Theory.setup