# HG changeset patch
# User wenzelm
# Date 1704551501 -3600
# Node ID 0875c87b4a4bf023c58ef1adc2fb5bca2686f126
# Parent  16c65e67dd754bb1dcf93a1a5dd3ac21867b0ff7
clarified signature;
clarified modules;

diff -r 16c65e67dd75 -r 0875c87b4a4b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Jan 06 13:13:48 2024 +0100
+++ b/src/Pure/proofterm.ML	Sat Jan 06 15:31:41 2024 +0100
@@ -182,10 +182,10 @@
   val export_proof_boxes_required: theory -> bool
   val export_proof_boxes: proof_body list -> unit
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
-  val thm_proof: theory -> ZTerm.sorts_zproof -> sorts_proof -> string * Position.T -> sort list ->
-    term list -> term -> (serial * proof_body future) list -> proof_body -> proof_body
-  val unconstrain_thm_proof: theory -> ZTerm.sorts_zproof -> sorts_proof ->
-    sort list -> term -> (serial * proof_body future) list -> proof_body -> term * proof_body
+  val thm_proof: theory -> sorts_proof -> string * Position.T -> sort list -> term list ->
+    term -> (serial * proof_body future) list -> proof_body -> proof_body
+  val unconstrain_thm_proof: theory -> sorts_proof -> sort list ->
+    term -> (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
@@ -2173,7 +2173,7 @@
       strict = false} xml
   end;
 
-fun prepare_thm_proof unconstrain thy sorts_zproof sorts_proof
+fun prepare_thm_proof unconstrain thy sorts_proof
     (name, pos) shyps hyps concl promises
     (PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zproof0, proof = proof0}) =
   let
@@ -2186,7 +2186,8 @@
 
     val proofs = get_proofs_level ();
     val (zproof1, zboxes1) =
-      if zproof_enabled proofs then ZTerm.add_box_proof thy hyps concl zproof0 zboxes0
+      if zproof_enabled proofs then
+        ZTerm.add_box_proof {unconstrain = unconstrain} thy hyps concl zproof0 zboxes0
       else (ZDummy, []);
     val proof1 =
       if proof_enabled proofs then fold_rev implies_intr_proof hyps proof0
@@ -2246,20 +2247,16 @@
       else map PClass (#outer_constraints ucontext) @ map Hyp hyps;
     val proof2 = proof_combP (proof_combt' (head, argst), argsP);
 
-    val (zboxes2, zproof2) =
-      if unconstrain then (zboxes1, zproof1)  (* FIXME proper zproof *)
-      else (zboxes1, zproof1);
-
-    val body2 = {oracles = [], thms = [thm], zboxes = zboxes2, zproof = zproof2, proof = proof2};
+    val body2 = {oracles = [], thms = [thm], zboxes = zboxes1, zproof = zproof1, proof = proof2};
   in (prop1, PBody body2) end;
 
 in
 
-fun thm_proof thy sorts_zproof sorts_proof name shyps hyps concl promises =
-  prepare_thm_proof false thy sorts_zproof sorts_proof name shyps hyps concl promises #> #2;
+fun thm_proof thy sorts_proof name shyps hyps concl promises =
+  prepare_thm_proof false thy sorts_proof name shyps hyps concl promises #> #2;
 
-fun unconstrain_thm_proof thy sorts_zproof sorts_proof shyps concl promises body =
-  prepare_thm_proof true thy sorts_zproof sorts_proof ("", Position.none)
+fun unconstrain_thm_proof thy sorts_proof shyps concl promises body =
+  prepare_thm_proof true thy sorts_proof ("", Position.none)
     shyps [] concl promises body;
 
 end;
diff -r 16c65e67dd75 -r 0875c87b4a4b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Jan 06 13:13:48 2024 +0100
+++ b/src/Pure/thm.ML	Sat Jan 06 15:31:41 2024 +0100
@@ -133,7 +133,7 @@
   (*type classes*)
   val the_classrel: theory -> class * class -> thm
   val the_arity: theory -> string * sort list * class -> thm
-  val sorts_zproof: theory -> ZTerm.sorts_zproof
+  val sorts_zproof: theory -> ZTerm.sorts_proof
   val sorts_proof: theory -> Proofterm.sorts_proof
   (*oracles*)
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
@@ -1157,9 +1157,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' =
-        Proofterm.thm_proof thy (sorts_zproof thy) (sorts_proof thy)
-          name_pos shyps hyps prop ps body;
+      val body' = Proofterm.thm_proof thy (sorts_proof thy) name_pos shyps hyps prop ps body;
     in Thm (make_deriv0 [] body', args) end);
 
 fun close_derivation pos =
@@ -2020,9 +2018,7 @@
       val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
-      val (prop', body') =
-        Proofterm.unconstrain_thm_proof thy (sorts_zproof thy) (sorts_proof thy)
-          shyps prop ps body;
+      val (prop', body') = Proofterm.unconstrain_thm_proof thy (sorts_proof thy) shyps prop ps body;
     in
       Thm (make_deriv0 [] body',
        {cert = cert,
diff -r 16c65e67dd75 -r 0875c87b4a4b src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Jan 06 13:13:48 2024 +0100
+++ b/src/Pure/zterm.ML	Sat Jan 06 15:31:41 2024 +0100
@@ -266,7 +266,8 @@
   type zboxes = zbox Ord_List.T
   val union_zboxes: zboxes -> zboxes -> zboxes
   val unions_zboxes: zboxes list -> zboxes
-  val add_box_proof: theory -> term list -> term -> zproof -> zboxes -> zproof * zboxes
+  val add_box_proof: {unconstrain: bool} -> theory ->
+    term list -> term -> zproof -> zboxes -> zproof * zboxes
   val thm_proof: theory -> Thm_Name.T * Position.T -> term list -> term -> zproof -> zbox * zproof
   val axiom_proof:  theory -> string -> term -> zproof
   val oracle_proof:  theory -> string -> term -> zproof
@@ -299,10 +300,10 @@
     zproof -> zproof
   val bicompose_proof: theory -> Envir.env -> int -> bool -> term list -> term list ->
     term option -> term list -> int -> int -> term list -> zproof -> zproof -> zproof
-  type sorts_zproof = (class * class -> zproof) * (string * class list list * class -> zproof)
-  val of_sort_proof: Sorts.algebra -> sorts_zproof -> (typ * class -> zproof) ->
+  type sorts_proof = (class * class -> zproof) * (string * class list list * class -> zproof)
+  val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> zproof) ->
     typ * sort -> zproof list
-  val unconstrainT_proof: theory -> sorts_zproof -> Logic.unconstrain_context -> zproof -> zproof
+  val unconstrainT_proof: theory -> sorts_proof -> Logic.unconstrain_context -> zproof -> zproof
 end;
 
 structure ZTerm: ZTERM =
@@ -880,8 +881,9 @@
     fun zproof_name i = ZThm {theory_name = thy_name, thm_name = thm_name, serial = i};
   in box_proof zproof_name thy end;
 
-fun add_box_proof thy hyps concl prf zboxes =
+fun add_box_proof {unconstrain} thy hyps concl prf zboxes =
   let
+    (* FIXME unconstrain *)
     val (zbox, prf') = box_proof ZBox thy hyps concl prf;
     val zboxes' = add_zboxes zbox zboxes;
   in (prf', zboxes') end;
@@ -1251,7 +1253,7 @@
 
 (* sort constraints within the logic *)
 
-type sorts_zproof = (class * class -> zproof) * (string * class list list * class -> zproof);
+type sorts_proof = (class * class -> zproof) * (string * class list list * class -> zproof);
 
 fun of_sort_proof algebra (classrel_proof, arity_proof) hyps =
   Sorts.of_sort_derivation algebra