# HG changeset patch
# User wenzelm
# Date 1703012537 -3600
# Node ID 8db60cadad86f5c2a5c447d63c58ee75c4d07445
# Parent  e4a9a861856bbc8958e17611a5145f39b6ec19f8
clarified signature;

diff -r e4a9a861856b -r 8db60cadad86 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Dec 19 19:20:21 2023 +0100
+++ b/src/Pure/proofterm.ML	Tue Dec 19 20:02:17 2023 +0100
@@ -2202,7 +2202,8 @@
 
     val proofs = get_proofs_level ();
     val (zboxes1, zproof1) =
-      if zproof_enabled proofs then ZTerm.box_proof thy hyps concl (#zboxes body0, #zproof body0)
+      if zproof_enabled proofs
+      then ZTerm.add_box_proof thy hyps concl (#zboxes body0, #zproof body0)
       else ([], ZDummy);
     val proof1 =
       if proof_enabled proofs then fold_rev implies_intr_proof hyps (#proof body0)
diff -r e4a9a861856b -r 8db60cadad86 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 19 19:20:21 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 19 20:02:17 2023 +0100
@@ -264,7 +264,8 @@
   type zboxes = zbox Ord_List.T
   val union_zboxes: zboxes -> zboxes -> zboxes
   val unions_zboxes: zboxes list -> zboxes
-  val box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof
+  val box_proof: theory -> term list -> term -> zproof -> zbox * zproof
+  val add_box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof
   val axiom_proof:  theory -> string -> term -> zproof
   val oracle_proof:  theory -> string -> term -> zproof
   val assume_proof: theory -> term -> zproof
@@ -786,7 +787,7 @@
 
 in
 
-fun box_proof thy hyps concl (zboxes: zboxes, prf) =
+fun box_proof thy hyps concl prf =
   let
     val {zterm, ...} = zterm_cache thy;
     val hyps' = map zterm hyps;
@@ -796,9 +797,13 @@
     val prf' = beta_norm_prooft (close_proof hyps' prf);
 
     val i = serial ();
-    val zboxes' = add_zboxes (i, (prop', prf')) zboxes;
-    val prf'' = ZAppts (ZConstp (zproof_const (ZBox i) prop'), hyps');
-  in (zboxes', prf'') end;
+    val zbox: zbox = (i, (prop', prf'));
+    val zbox_prf = ZAppts (ZConstp (zproof_const (ZBox i) prop'), hyps');
+  in (zbox, zbox_prf) end;
+
+fun add_box_proof thy hyps concl (zboxes, prf) =
+  let val (zbox, zbox_prf) = box_proof thy hyps concl prf
+  in (add_zboxes zbox zboxes, zbox_prf) end;
 
 end;