# HG changeset patch
# User wenzelm
# Date 1702153526 -3600
# Node ID 936ad4627a74c308bf915603339bc01b8efa8d07
# Parent  78d032205af41ce627f8e9753ca20369e91f703d
tuned;

diff -r 78d032205af4 -r 936ad4627a74 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 09 21:15:12 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 09 21:25:26 2023 +0100
@@ -784,10 +784,6 @@
     else empty_deriv
   end;
 
-fun deriv_rule_unconditional (f, g)
-    (Deriv {promises, body = PBody {oracles, thms, zboxes, zproof = zprf, proof = prf}}) =
-  make_deriv promises oracles thms zboxes (g zprf) (f prf);
-
 
 (* fulfilled proofs *)
 
@@ -1074,9 +1070,11 @@
 
         val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints;
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
+
+        val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
+        val proof' = Proofterm.strip_shyps_proof algebra present witnessed extra' proof;
       in
-        Thm (deriv_rule_unconditional
-          (Proofterm.strip_shyps_proof algebra present witnessed extra', I) der,
+        Thm (make_deriv promises oracles thms zboxes zproof proof',
          {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
       end)