# HG changeset patch
# User wenzelm
# Date 1703617885 -3600
# Node ID c28d4d1986f1d48c3fd6dda0612c0a4d812e3a76
# Parent  da22c8ab0112ccca4683cd360596a97fc255eb4f
tuned signature;

diff -r da22c8ab0112 -r c28d4d1986f1 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Tue Dec 26 20:06:30 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 26 20:11:25 2023 +0100
@@ -198,7 +198,7 @@
     ZAxiom of string
   | ZOracle of string
   | ZBox of serial
-  | ZThm of {theory_name: string, thm_name: Thm_Name.T, pos: Position.T, serial: int};
+  | ZThm of {theory_name: string, thm_name: Thm_Name.T * Position.T, serial: int};
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
@@ -817,10 +817,10 @@
 
 in
 
-fun thm_proof thy (name, pos) =
+fun thm_proof thy thm_name =
   let
     val thy_name = Context.theory_long_name thy;
-    fun zproof_name i = ZThm {theory_name = thy_name, thm_name = name, pos = pos, serial = i};
+    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) =