# HG changeset patch
# User wenzelm
# Date 1702552869 -3600
# Node ID 64c655e8e8bf59134ffef155fbc92b8331efa47d
# Parent  2e6fcc331f10ad05d6aad4bf105c7763895b02f1
clarified modules;

diff -r 2e6fcc331f10 -r 64c655e8e8bf src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Dec 13 23:05:41 2023 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 14 12:21:09 2023 +0100
@@ -191,10 +191,10 @@
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> string * Position.T -> sort list ->
-    term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof
+    term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof_body
   val unconstrain_thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> sort list -> term ->
-    (serial * proof_body future) list -> proof_body -> thm * proof
+    (serial * proof_body future) list -> proof_body -> thm * proof_body
   val get_identity: sort list -> term list -> term -> proof ->
     {serial: serial, theory_name: string, name: string} option
   val get_approximative_name: sort list -> term list -> term -> proof -> string
@@ -2257,7 +2257,11 @@
       else
         proof_combP (proof_combt' (head, args),
           map PClass (#outer_constraints ucontext) @ map Hyp hyps);
-  in (thm, proof) end;
+    val zproof = ZTerm.todo_proof ();
+
+    val proof_body =
+      PBody {oracles = [], thms = [thm], zboxes = empty_zboxes, zproof = zproof, proof = proof};
+  in (thm, proof_body) end;
 
 in
 
diff -r 2e6fcc331f10 -r 64c655e8e8bf src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Dec 13 23:05:41 2023 +0100
+++ b/src/Pure/thm.ML	Thu Dec 14 12:21:09 2023 +0100
@@ -744,9 +744,11 @@
 
 (** derivations and promised proofs **)
 
+fun make_deriv0 promises body = Deriv {promises = promises, body = body};
+
 fun make_deriv promises oracles thms zboxes zproof proof =
-  Deriv {promises = promises,
-    body = PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof}};
+  make_deriv0 promises
+    (PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof});
 
 val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes ZDummy MinProof;
 
@@ -1027,7 +1029,7 @@
         val body' =
           PBody {oracles = oracles', thms = thms', zboxes = zboxes', zproof = zproof, proof = proof};
       in
-        Thm (Deriv {promises = promises, body = body'},
+        Thm (make_deriv0 promises body',
           {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
             shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})
       end;
@@ -1128,12 +1130,10 @@
       val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
-      val (pthm, prf) =
+      val (_, body') =
         Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
           name_pos shyps hyps prop ps body;
-      val zprf = ZTerm.todo_proof (Proofterm.zproof_of body);
-      val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes zprf prf;
-    in Thm (der', args) end);
+    in Thm (make_deriv0 [] body', args) end);
 
 fun close_derivation pos =
   solve_constraints #> (fn thm =>
@@ -1929,14 +1929,12 @@
       val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
-      val (pthm, prf) =
+      val ((_, thm_node), body') =
         Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
           shyps prop ps body;
-      val zprf = ZTerm.todo_proof body;
-      val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes zprf prf;
-      val prop' = Proofterm.thm_node_prop (#2 pthm);
+      val prop' = Proofterm.thm_node_prop thm_node;
     in
-      Thm (der',
+      Thm (make_deriv0 [] body',
        {cert = cert,
         tags = [],
         maxidx = maxidx_of_term prop',