tuned signature, following Proofterm.thm_header;

--- a/src/Pure/zterm.ML	Tue Dec 26 12:46:10 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 26 20:06:30 2023 +0100
@@ -198,7 +198,7 @@
     ZAxiom of string
   | ZOracle of string
   | ZBox of serial
-  | ZThm of {theory_long_name: string, thm_name: Thm_Name.T, pos: Position.T, serial: int};
+  | ZThm of {theory_name: string, thm_name: Thm_Name.T, pos: Position.T, serial: int};
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
@@ -820,8 +820,7 @@
 fun thm_proof thy (name, pos) =
   let
     val thy_name = Context.theory_long_name thy;
-    fun zproof_name i =
-      ZThm {theory_long_name = thy_name, thm_name = name, pos = pos, serial = i};
+    fun zproof_name i = ZThm {theory_name = thy_name, thm_name = name, pos = pos, serial = i};
   in box_proof zproof_name thy end;
 
 fun add_box_proof thy hyps concl (zboxes, prf) =