diff -r ea908185a597 -r 979f3893aa37 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jun 06 12:42:42 2024 +0200
+++ b/src/Pure/zterm.ML	Thu Jun 06 12:53:02 2024 +0200
@@ -195,8 +195,8 @@
 datatype zproof_name =
     ZAxiom of string
   | ZOracle of string
-  | ZBox of serial
-  | ZThm of {theory_name: string, thm_name: Thm_Name.T * Position.T, serial: int};
+  | ZBox of {theory_name: string, serial: serial}
+  | ZThm of {theory_name: string, thm_name: Thm_Name.T * Position.T, serial: serial};
 
 type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
 
@@ -915,7 +915,9 @@
 
 fun add_box_proof unconstrain thy hyps concl prf zboxes =
   let
-    val (zbox, prf') = box_proof unconstrain ZBox thy hyps concl prf;
+    val thy_name = Context.theory_long_name thy;
+    fun zproof_name i = ZBox {theory_name = thy_name, serial = i};
+    val (zbox, prf') = box_proof unconstrain zproof_name thy hyps concl prf;
     val zboxes' = add_zboxes zbox zboxes;
   in (prf', zboxes') end;