# HG changeset patch
# User wenzelm
# Date 1635416093 -7200
# Node ID 722b40f8d7645e50f16cd3f7b6d1882281d69bee
# Parent  b7804cff55d9c897a508c2cd4349d6bd3d7c8730
tuned;

diff -r b7804cff55d9 -r 722b40f8d764 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Thu Oct 28 12:09:58 2021 +0200
+++ b/src/Pure/ML/ml_thms.ML	Thu Oct 28 12:14:53 2021 +0200
@@ -79,18 +79,18 @@
   (ML_Antiquotation.declaration \<^binding>\<open>lemma\<close>
     (Scan.lift (Args.mode "open" -- Parse.and_list1 (Scan.repeat1 Parse.embedded_inner_syntax) --
       Method.parse_by))
-    (fn _ => fn ((is_open, raw_propss), (methods, reports)) => fn ctxt =>
+    (fn _ => fn ((is_open, raw_stmt), (methods, reports)) => fn ctxt =>
       let
         val _ = Context_Position.reports ctxt reports;
 
-        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
+        val stmt = burrow (map (rpair []) o Syntax.read_props 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
-          |> Proof.theorem NONE after_qed propss
+          |> Proof.theorem NONE after_qed stmt
           |> Proof.global_terminal_proof methods;
         val thms =
           Proof_Context.get_fact ctxt'