# HG changeset patch
# User wenzelm
# Date 1703261948 -3600
# Node ID 6d167422bcb058027bb29e5f6a1a1da8e0ac7319
# Parent  afd26cc61e8d9dfb8c80badbe79744f2eadb7ed7
clarified signature;

diff -r afd26cc61e8d -r 6d167422bcb0 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 22 17:18:32 2023 +0100
+++ b/src/Pure/thm.ML	Fri Dec 22 17:19:08 2023 +0100
@@ -173,8 +173,9 @@
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
-  val get_zproof: theory -> serial ->
-    {thm_name: Thm_Name.T, pos: Position.T, prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} option
+  type stored_zproof =
+    {name: Thm_Name.T * Position.T, prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof}
+  val get_zproof: theory -> serial -> stored_zproof option
   val store_zproof: Thm_Name.T * Position.T -> thm -> theory -> thm * theory
   val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
@@ -944,7 +945,7 @@
 (* data *)
 
 type stored_zproof =
-  {thm_name: Thm_Name.T, pos: Position.T, prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof};
+  {name: Thm_Name.T * Position.T, prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof};
 
 structure Data = Theory_Data
 (
@@ -2082,19 +2083,19 @@
 
 val get_zproof = Inttab.lookup o get_zproofs;
 
-fun store_zproof (name, pos) thm thy =
+fun store_zproof name thm thy =
   let
     val Thm (Deriv {promises, body = PBody body}, args as {hyps, prop, ...}) = thm;
     val {oracles, thms, zboxes, zproof, proof} = body;
     val _ = null promises orelse
       raise THM ("store_zproof: theorem may not use promises", 0, [thm]);
 
-    val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy (name, pos) hyps prop zproof;
+    val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy name hyps prop zproof;
     val (zboxes', zprf') =
       if Options.default_bool "prune_proofs" then ([], ZDummy) else (zboxes, zprf);
     val thy' = thy
       |> (map_zproofs o Inttab.update)
-          (i, {thm_name = name, pos = pos, prop = zprop, zboxes = zboxes', zproof = zprf'});
+          (i, {name = name, prop = zprop, zboxes = zboxes', zproof = zprf'});
     val der' = make_deriv promises oracles thms [] zproof' proof;
   in (Thm (der', args), thy') end;