# HG changeset patch
# User wenzelm
# Date 1703253355 -3600
# Node ID 40cabd57aac34d9f3ceba053a3f0171fc8f5ad61
# Parent  8e0c80a9beb6af3378615b437bba5660df7ca59d
clarified signature;

diff -r 8e0c80a9beb6 -r 40cabd57aac3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Dec 22 13:53:03 2023 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 22 14:55:55 2023 +0100
@@ -188,10 +188,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_body
+    term list -> term -> (serial * proof_body future) list -> proof_body -> 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_body
+    (serial * proof_body future) list -> proof_body -> term * 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
@@ -2265,11 +2265,12 @@
       else (zboxes1, zproof1);
 
     val body2 = {oracles = [], thms = [thm], zboxes = zboxes2, zproof = zproof2, proof = proof2};
-  in (thm, PBody body2) end;
+  in (prop1, PBody body2) end;
 
 in
 
-fun thm_proof thy = prepare_thm_proof false thy;
+fun thm_proof thy classrel_proof arity_proof name shyps hyps concl promises =
+  prepare_thm_proof false thy classrel_proof arity_proof name shyps hyps concl promises #> #2;
 
 fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body =
   prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none)
diff -r 8e0c80a9beb6 -r 40cabd57aac3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 22 13:53:03 2023 +0100
+++ b/src/Pure/thm.ML	Fri Dec 22 14:55:55 2023 +0100
@@ -1142,7 +1142,7 @@
       val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
-      val (_, body') =
+      val body' =
         Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
           name_pos shyps hyps prop ps body;
     in Thm (make_deriv0 [] body', args) end);
@@ -2005,10 +2005,9 @@
       val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
-      val ((_, thm_node), body') =
+      val (prop', body') =
         Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
           shyps prop ps body;
-      val prop' = Proofterm.thm_node_prop thm_node;
     in
       Thm (make_deriv0 [] body',
        {cert = cert,