# HG changeset patch
# User wenzelm
# Date 1703003472 -3600
# Node ID 3114c98738e631c0eb42630fad2c7eea785289fe
# Parent  816472c38979132e64a7cd09d1c719c41310608d
tuned;

diff -r 816472c38979 -r 3114c98738e6 src/Pure/thm.ML
--- 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;