# HG changeset patch
# User wenzelm
# Date 1702900679 -3600
# Node ID d9a7ee1bd0708f6d3fa78c80319c1e5c00226bb4
# Parent  8943cc46a66f277078733da02f1f523f6be9a462
minor performance tuning: more concise union;

diff -r 8943cc46a66f -r d9a7ee1bd070 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Dec 18 12:02:58 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Dec 18 12:57:59 2023 +0100
@@ -184,7 +184,7 @@
       PBody
        {oracles = Ord_List.make Proofterm.oracle_ord oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
-        zboxes = ZTerm.empty_zboxes,
+        zboxes = [],
         zproof = ZDummy,
         proof = prf};
   in Proofterm.thm_body body end;
diff -r 8943cc46a66f -r d9a7ee1bd070 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Dec 18 12:02:58 2023 +0100
+++ b/src/Pure/proofterm.ML	Mon Dec 18 12:57:59 2023 +0100
@@ -339,7 +339,7 @@
 val unions_thms = Ord_List.unions thm_ord;
 
 fun no_proof_body zproof proof =
-  PBody {oracles = [], thms = [], zboxes = ZTerm.empty_zboxes, zproof = zproof, proof = proof};
+  PBody {oracles = [], thms = [], zboxes = [], zproof = zproof, proof = proof};
 val no_thm_body = thm_body (no_proof_body ZDummy MinProof);
 
 fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
@@ -463,7 +463,7 @@
     val (a, b, c) =
       triple (list (pair (pair string (Position.of_properties o properties))
         (option (term consts)))) (list (thm consts)) (proof consts) x;
-  in PBody {oracles = a, thms = b, zboxes = ZTerm.empty_zboxes, zproof = ZDummy, proof = c} end
+  in PBody {oracles = a, thms = b, zboxes = [], zproof = ZDummy, proof = c} end
 and thm consts x =
   let
     val (a, (b, (c, (d, e)))) =
@@ -1982,7 +1982,9 @@
         (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
     val thms =
       unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
-    val zboxes = fold (fn (_, PBody {zboxes, ...}) => ZTerm.union_zboxes zboxes) ps zboxes0;
+    val zboxes =
+      ZTerm.unions_zboxes
+        (fold (fn (_, PBody {zboxes, ...}) => not (null zboxes) ? cons zboxes) ps [zboxes0]);
     val proof = rew_proof thy proof0;
   in
     PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof}
@@ -2197,7 +2199,7 @@
     val proofs = get_proofs_level ();
     val (zboxes1, zproof1) =
       if zproof_enabled proofs then ZTerm.box_proof thy hyps concl (#zboxes body0, #zproof body0)
-      else (ZTerm.empty_zboxes, ZDummy);
+      else ([], ZDummy);
     val proof1 =
       if proof_enabled proofs then fold_rev implies_intr_proof hyps (#proof body0)
       else MinProof;
diff -r 8943cc46a66f -r d9a7ee1bd070 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Dec 18 12:02:58 2023 +0100
+++ b/src/Pure/thm.ML	Mon Dec 18 12:57:59 2023 +0100
@@ -750,7 +750,7 @@
   make_deriv0 promises
     (PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof});
 
-val empty_deriv = make_deriv [] [] [] ZTerm.empty_zboxes ZDummy MinProof;
+val empty_deriv = make_deriv [] [] [] [] ZDummy MinProof;
 
 
 (* inference rules *)
@@ -780,7 +780,7 @@
 fun deriv_rule0 zproof proof =
   let val proofs = Proofterm.get_proofs_level () in
     if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
-      deriv_rule1 I I (make_deriv [] [] [] ZTerm.empty_zboxes
+      deriv_rule1 I I (make_deriv [] [] [] []
        (if Proofterm.zproof_enabled proofs then zproof () else ZDummy)
        (if Proofterm.proof_enabled proofs then proof () else MinProof))
     else empty_deriv
@@ -844,7 +844,7 @@
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv [(i, future)] [] [] ZTerm.empty_zboxes ZDummy MinProof,
+    Thm (make_deriv [(i, future)] [] [] [] ZDummy MinProof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -985,7 +985,7 @@
 
 local
 
-val empty_digest = ([], [], ZTerm.empty_zboxes);
+val empty_digest = ([], [], []);
 
 fun union_digest (oracles1, thms1, zboxes1) (oracles2, thms2, zboxes2) =
  (Proofterm.union_oracles oracles1 oracles2,
@@ -1171,7 +1171,7 @@
               then ZTerm.oracle_proof (Context.certificate_theory cert) name prop
               else ZDummy;
           in
-            Thm (make_deriv [] [oracle] [] ZTerm.empty_zboxes zproof proof,
+            Thm (make_deriv [] [oracle] [] [] zproof proof,
              {cert = cert,
               tags = [],
               maxidx = maxidx,
diff -r 8943cc46a66f -r d9a7ee1bd070 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Mon Dec 18 12:02:58 2023 +0100
+++ b/src/Pure/zterm.ML	Mon Dec 18 12:57:59 2023 +0100
@@ -247,9 +247,11 @@
   val norm_type: Type.tyenv -> ztyp -> ztyp
   val norm_term: theory -> Envir.env -> zterm -> zterm
   val norm_proof: theory -> Envir.env -> term list -> zproof -> zproof
-  type zboxes = (zterm * zproof future) Inttab.table
-  val empty_zboxes: zboxes
+  type zbox = serial * (zterm * zproof future)
+  val zbox_ord: zbox ord
+  type zboxes = zbox Ord_List.T
   val union_zboxes: zboxes -> zboxes -> zboxes
+  val unions_zboxes: zboxes list -> zboxes
   val box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof
   val axiom_proof:  theory -> string -> term -> zproof
   val oracle_proof:  theory -> string -> term -> zproof
@@ -660,11 +662,13 @@
 
 (* closed proof boxes *)
 
-type zboxes = (zterm * zproof future) Inttab.table;
+type zbox = serial * (zterm * zproof future);
+val zbox_ord: zbox ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
-val empty_zboxes: zboxes = Inttab.empty;
-val union_zboxes: zboxes -> zboxes -> zboxes = curry (Inttab.merge (K true));
-fun add_zboxes entry : zboxes -> zboxes = Inttab.update_new entry;
+type zboxes = zbox Ord_List.T;
+val union_zboxes = Ord_List.union zbox_ord;
+val unions_zboxes = Ord_List.unions zbox_ord;
+val add_zboxes = Ord_List.insert zbox_ord;
 
 local