--- a/src/Pure/proofterm.ML Thu Jan 04 15:56:03 2024 +0100
+++ b/src/Pure/proofterm.ML Sat Jan 06 12:34:55 2024 +0100
@@ -2184,10 +2184,10 @@
val (ucontext as {typ_operation, ...}, prop1) = Logic.unconstrainT shyps prop;
val proofs = get_proofs_level ();
- val (zboxes1, zproof1) =
+ val (zproof1, zboxes1) =
if zproof_enabled proofs
- then ZTerm.add_box_proof thy hyps concl (#zboxes body0, #zproof body0)
- else ([], ZDummy);
+ then ZTerm.add_box_proof thy hyps concl (#zproof body0) (#zboxes body0)
+ else (ZDummy, []);
val proof1 =
if proof_enabled proofs then fold_rev implies_intr_proof hyps (#proof body0)
else MinProof;
--- a/src/Pure/zterm.ML Thu Jan 04 15:56:03 2024 +0100
+++ b/src/Pure/zterm.ML Sat Jan 06 12:34:55 2024 +0100
@@ -266,7 +266,7 @@
type zboxes = zbox Ord_List.T
val union_zboxes: zboxes -> zboxes -> zboxes
val unions_zboxes: zboxes list -> zboxes
- val add_box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof
+ val add_box_proof: theory -> term list -> term -> zproof -> zboxes -> zproof * zboxes
val thm_proof: theory -> Thm_Name.T * Position.T -> term list -> term -> zproof -> zbox * zproof
val axiom_proof: theory -> string -> term -> zproof
val oracle_proof: theory -> string -> term -> zproof
@@ -880,9 +880,11 @@
fun zproof_name i = ZThm {theory_name = thy_name, thm_name = thm_name, serial = i};
in box_proof zproof_name thy end;
-fun add_box_proof thy hyps concl (zboxes, prf) =
- let val (zbox, zbox_prf) = box_proof ZBox thy hyps concl prf
- in (add_zboxes zbox zboxes, zbox_prf) end;
+fun add_box_proof thy hyps concl prf zboxes =
+ let
+ val (zbox, prf') = box_proof ZBox thy hyps concl prf;
+ val zboxes' = add_zboxes zbox zboxes;
+ in (prf', zboxes') end;
end;