# HG changeset patch
# User wenzelm
# Date 1703617590 -3600
# Node ID da22c8ab0112ccca4683cd360596a97fc255eb4f
# Parent  5b01b93de0627011fcf9584f4fc8257cce8bf646
tuned signature, following Proofterm.thm_header;

diff -r 5b01b93de062 -r da22c8ab0112 src/Pure/zterm.ML
--- 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) =