performance tuning: replace Ord_List by Set();

--- a/src/Doc/Implementation/Logic.thy	Tue Apr 11 13:23:46 2023 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Apr 11 15:03:02 2023 +0200
@@ -701,7 +701,7 @@
   \begin{mldecls}
   @{define_ML Theory.add_deps: "Defs.context -> string ->
   Defs.entry -> Defs.entry list -> theory -> theory"} \\
-  @{define_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\
+  @{define_ML Thm_Deps.all_oracles: "thm list -> Oracles.T"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Logic.all\<close>~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where

--- a/src/HOL/Examples/Iff_Oracle.thy	Tue Apr 11 13:23:46 2023 +0200
+++ b/src/HOL/Examples/Iff_Oracle.thy	Tue Apr 11 15:03:02 2023 +0200
@@ -36,7 +36,8 @@
 ML \<open>iff_oracle (\<^theory>, 10)\<close>
 
 ML \<open>
-  \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
+  \<^assert> (map (#1 o #1) (Oracles.dest (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)])) =
+    [\<^oracle_name>\<open>iff_oracle\<close>]);
 \<close>
 
 text \<open>These oracle calls had better fail.\<close>

--- a/src/Pure/Proof/extraction.ML	Tue Apr 11 13:23:46 2023 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Apr 11 15:03:02 2023 +0200
@@ -182,7 +182,7 @@
           | _ => I);
     val body =
       PBody
-       {oracles = Ord_List.make Proofterm.oracle_ord oracles,
+       {oracles = Oracles.make oracles,
         thms = Ord_List.make Proofterm.thm_ord thms,
         proof = prf};
   in Proofterm.thm_body body end;

--- a/src/Pure/proofterm.ML	Tue Apr 11 13:23:46 2023 +0200
+++ b/src/Pure/proofterm.ML	Tue Apr 11 15:03:02 2023 +0200
@@ -6,6 +6,11 @@
 
 infix 8 % %% %>;
 
+structure Oracles = Set(
+  type key = (string * Position.T) * term option
+  val ord = prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord)
+);
+
 signature PROOFTERM =
 sig
   type thm_header =
@@ -26,10 +31,9 @@
    | Oracle of string * term * typ list option
    | PThm of thm_header * thm_body
   and proof_body = PBody of
-    {oracles: ((string * Position.T) * term option) Ord_List.T,
+    {oracles: Oracles.T,
      thms: (serial * thm_node) Ord_List.T,
      proof: proof}
-  type oracle = (string * Position.T) * term option
   type thm = serial * thm_node
   exception MIN_PROOF of unit
   val proof_of: proof_body -> proof
@@ -51,9 +55,7 @@
   val fold_body_thms:
     ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     proof_body list -> 'a -> 'a
-  val oracle_ord: oracle ord
   val thm_ord: thm ord
-  val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
   val unions_thms: thm Ord_List.T list -> thm Ord_List.T
   val no_proof_body: proof -> proof_body
   val no_thm_names: proof -> proof
@@ -217,7 +219,7 @@
  | Oracle of string * term * typ list option
  | PThm of thm_header * thm_body
 and proof_body = PBody of
-  {oracles: ((string * Position.T) * term option) Ord_List.T,
+  {oracles: Oracles.T,
    thms: (serial * thm_node) Ord_List.T,
    proof: proof}
 and thm_body =
@@ -226,10 +228,6 @@
   Thm_Node of {theory_name: string, name: string, prop: term,
     body: proof_body future, export: unit lazy, consolidate: unit lazy};
 
-type oracle = (string * Position.T) * term option;
-val oracle_ord: oracle ord =
-  prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord);
-
 type thm = serial * thm_node;
 val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
@@ -316,10 +314,9 @@
 
 (* proof body *)
 
-val unions_oracles = Ord_List.unions oracle_ord;
 val unions_thms = Ord_List.unions thm_ord;
 
-fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
+fun no_proof_body proof = PBody {oracles = Oracles.empty, thms = [], proof = proof};
 val no_thm_body = thm_body (no_proof_body MinProof);
 
 fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
@@ -375,7 +372,7 @@
         (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
 and proof_body consts (PBody {oracles, thms, proof = prf}) =
   triple (list (pair (pair string (properties o Position.properties_of))
-      (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
+      (option (term consts)))) (list (thm consts)) (proof consts) (Oracles.dest oracles, thms, prf)
 and thm consts (a, thm_node) =
   pair int (pair string (pair string (pair (term consts) (proof_body consts))))
     (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
@@ -441,7 +438,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, proof = c} end
+  in PBody {oracles = Oracles.make a, thms = b, proof = c} end
 and thm consts x =
   let
     val (a, (b, (c, (d, e)))) =
@@ -1990,8 +1987,9 @@
     val _ = consolidate_bodies (map #2 ps @ [body0]);
     val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
     val oracles =
-      unions_oracles
-        (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
+      Oracles.merges
+        (fold (fn (_, PBody {oracles, ...}) => not (Oracles.is_empty oracles) ? cons oracles)
+          ps [oracles0]);
     val thms =
       unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
     val proof = rew_proof thy proof0;

--- a/src/Pure/thm.ML	Tue Apr 11 13:23:46 2023 +0200
+++ b/src/Pure/thm.ML	Tue Apr 11 15:03:02 2023 +0200
@@ -739,7 +739,7 @@
 fun make_deriv promises oracles thms proof =
   Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
 
-val empty_deriv = make_deriv empty_promises [] [] MinProof;
+val empty_deriv = make_deriv empty_promises Oracles.empty [] MinProof;
 
 
 (* inference rules *)
@@ -752,7 +752,7 @@
     (Deriv {promises = promises2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
   let
     val ps = merge_promises (promises1, promises2);
-    val oracles = Proofterm.unions_oracles [oracles1, oracles2];
+    val oracles = Oracles.merge (oracles1, oracles2);
     val thms = Proofterm.unions_thms [thms1, thms2];
     val prf =
       (case ! Proofterm.proofs of
@@ -766,7 +766,7 @@
 
 fun deriv_rule0 make_prf =
   if ! Proofterm.proofs <= 1 then empty_deriv
-  else deriv_rule1 I (make_deriv empty_promises [] [] (make_prf ()));
+  else deriv_rule1 I (make_deriv empty_promises Oracles.empty [] (make_prf ()));
 
 fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
   make_deriv promises oracles thms (f proof);
@@ -832,7 +832,7 @@
     val i = serial ();
     val future = future_thm |> Future.map (future_result i cert sorts prop);
   in
-    Thm (make_deriv (make_promises [(i, future)]) [] [] MinProof,
+    Thm (make_deriv (make_promises [(i, future)]) Oracles.empty [] MinProof,
      {cert = cert,
       tags = [],
       maxidx = maxidx,
@@ -974,7 +974,7 @@
 local
 
 fun union_digest (oracles1, thms1) (oracles2, thms2) =
-  (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]);
+  (Oracles.merge (oracles1, oracles2), Proofterm.unions_thms [thms1, thms2]);
 
 fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
   (oracles, thms);
@@ -982,11 +982,11 @@
 fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
   Sorts.of_sort_derivation (Sign.classes_of thy)
    {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 =>
-      if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
+      if c1 = c2 then (Oracles.empty, []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
     type_constructor = fn (a, _) => fn dom => fn c =>
       let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c))
       in (fold o fold) (union_digest o #1) dom arity_digest end,
-    type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)}
+    type_variable = fn T => map (pair (Oracles.empty, [])) (Type.sort_of_atyp T)}
    (typ, sort);
 
 in
@@ -1114,7 +1114,7 @@
       val (pthm, proof) =
         Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
           name_pos shyps (Termset.dest hyps) prop ps body;
-      val der' = make_deriv empty_promises [] [pthm] proof;
+      val der' = make_deriv empty_promises Oracles.empty [pthm] proof;
     in Thm (der', args) end);
 
 fun close_derivation pos =
@@ -1145,7 +1145,7 @@
               | 0 => (((name, Position.none), NONE), MinProof)
               | i => bad_proofs i);
           in
-            Thm (make_deriv empty_promises [oracle] [] prf,
+            Thm (make_deriv empty_promises (Oracles.make [oracle]) [] prf,
              {cert = Context.join_certificate (Context.Certificate thy', cert2),
               tags = [],
               maxidx = maxidx,
@@ -1805,7 +1805,7 @@
       val (pthm, proof) =
         Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
           shyps prop ps body;
-      val der' = make_deriv empty_promises [] [pthm] proof;
+      val der' = make_deriv empty_promises Oracles.empty [pthm] proof;
       val prop' = Proofterm.thm_node_prop (#2 pthm);
     in
       Thm (der',

--- a/src/Pure/thm_deps.ML	Tue Apr 11 13:23:46 2023 +0200
+++ b/src/Pure/thm_deps.ML	Tue Apr 11 15:03:02 2023 +0200
@@ -7,7 +7,7 @@
 
 signature THM_DEPS =
 sig
-  val all_oracles: thm list -> Proofterm.oracle list
+  val all_oracles: thm list -> Oracles.T
   val has_skip_proof: thm list -> bool
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
   val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
@@ -23,17 +23,17 @@
 fun all_oracles thms =
   let
     fun collect (PBody {oracles, thms, ...}) =
-      (if null oracles then I else apfst (cons oracles)) #>
+      (if Oracles.is_empty oracles then I else apfst (cons oracles)) #>
       (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
         if Intset.member seen i then (res, seen)
         else
           let val body = Future.join (Proofterm.thm_node_body thm_node)
           in collect body (res, Intset.insert i seen) end));
     val bodies = map Thm.proof_body_of thms;
-  in fold collect bodies ([], Intset.empty) |> #1 |> Proofterm.unions_oracles end;
+  in fold collect bodies ([], Intset.empty) |> #1 |> Oracles.merges end;
 
 fun has_skip_proof thms =
-  all_oracles thms |> exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>);
+  all_oracles thms |> Oracles.exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>);
 
 fun pretty_thm_oracles ctxt thms =
   let
@@ -44,7 +44,7 @@
           prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop];
     val oracles =
       (case try all_oracles thms of
-        SOME oracles => oracles
+        SOME oracles => Oracles.dest oracles
       | NONE => error "Malformed proofs")
   in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) oracles) end;