# HG changeset patch
# User wenzelm
# Date 1703619218 -3600
# Node ID 2187de552bd401e26065f19a83b77a54ef0a0d0f
# Parent  c28d4d1986f1d48c3fd6dda0612c0a4d812e3a76
clarified stored data: actual thm allows to replay zproofs in a modular manner;

diff -r c28d4d1986f1 -r 2187de552bd4 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 26 20:11:25 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 26 20:33:38 2023 +0100
@@ -173,9 +173,7 @@
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
-  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 get_zproof: theory -> serial -> {name: Thm_Name.T * Position.T, thm: thm} 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,13 +942,10 @@
 
 (* data *)
 
-type stored_zproof =
-  {name: Thm_Name.T * Position.T, prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof};
-
 structure Data = Theory_Data
 (
   type T =
-    stored_zproof Inttab.table *  (*stored thms: zproof*)
+    {name: Thm_Name.T * Position.T, thm: thm} Inttab.table *  (*stored zproof thms*)
     unit Name_Space.table *  (*oracles: authentic derivation names*)
     classes;  (*type classes within the logic*)
 
@@ -2087,17 +2082,16 @@
   let
     val Thm (Deriv {promises, body = PBody body}, args as {hyps, prop, ...}) = thm;
     val {oracles, thms, zboxes, zproof, proof} = body;
+    fun deriv a b = make_deriv promises oracles thms a b proof;
+
     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 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, {name = name, prop = zprop, zboxes = zboxes', zproof = zprf'});
-    val der' = make_deriv promises oracles thms [] zproof' proof;
-  in (Thm (der', args), thy') end;
+    val ((i, (_, zproof1)), zproof2) = ZTerm.thm_proof thy name hyps prop zproof;
+    val der1 = if Options.default_bool "prune_proofs" then deriv [] ZDummy else deriv zboxes zproof1;
+    val der2 = deriv [] zproof2;
+    val thy' = thy |> (map_zproofs o Inttab.update) (i, {name = name, thm = Thm (der1, args)});
+  in (Thm (der2, args), thy') end;