# HG changeset patch
# User wenzelm
# Date 1704717105 -3600
# Node ID 236d866ead4efe65e2f0ee4d7737d38bc8c24ab5
# Parent  2e834ee3b348dfcf1db3d27cd4fa643e0723152b
tuned signature;

diff -r 2e834ee3b348 -r 236d866ead4e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jan 08 12:08:31 2024 +0100
+++ b/src/Pure/thm.ML	Mon Jan 08 13:31:45 2024 +0100
@@ -175,7 +175,8 @@
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
   val get_zproof_serials: theory -> serial list
-  val get_zproof: theory -> serial -> {name: Thm_Name.T * Position.T, thm: thm} option
+  val get_zproof: theory -> serial ->
+    {name: Thm_Name.T * Position.T, thm: thm, zboxes: ZTerm.zboxes, zproof: 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
@@ -2095,8 +2096,11 @@
 val get_zproof_serials = Inttab.keys o get_zproofs;
 
 fun get_zproof thy =
-  Inttab.lookup (get_zproofs thy)
-  #> Option.map (fn {name, thm} => {name = name, thm = transfer thy thm});
+  Inttab.lookup (get_zproofs thy) #> Option.map (fn {name, thm} =>
+    let
+      val thm' = transfer thy thm;
+      val PBody {zboxes, zproof, ...} = proof_body_of thm';
+    in {name = name, thm = thm', zboxes = zboxes, zproof = zproof} end);
 
 fun store_zproof name thm thy =
   let