--- 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'