# 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>\lemma\ (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'