# HG changeset patch
# User wenzelm
# Date 1704540895 -3600
# Node ID 371ee5494d1584f5977700a433023b410d973295
# Parent  17e06494a4da374b3c31cdc46f00b41dd5e17503
tuned signature: canonical argument order;

diff -r 17e06494a4da -r 371ee5494d15 src/Pure/proofterm.ML
--- 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;
diff -r 17e06494a4da -r 371ee5494d15 src/Pure/zterm.ML
--- 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;