tuned;

--- a/src/Pure/thm.ML	Tue Dec 19 17:26:30 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 19 17:31:12 2023 +0100
@@ -1022,10 +1022,8 @@
         val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
         val (oracles', thms') = (oracles, thms)
           |> fold (fold union_digest o constraint_digest) constraints;
-        val body' =
-          PBody {oracles = oracles', thms = thms', zboxes = zboxes, zproof = zproof, proof = proof};
       in
-        Thm (make_deriv0 promises body',
+        Thm (make_deriv promises oracles' thms' zboxes zproof proof,
           {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
             shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})
       end;