# HG changeset patch
# User wenzelm
# Date 1681205059 -7200
# Node ID 15edec78869c044415f8edf9e9bed290f765060b
# Parent  d2645d3ad9e9fc87790222917d7e323f17a02bea
performance tuning: replace Table() by Set();

diff -r d2645d3ad9e9 -r 15edec78869c src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 11 11:16:33 2023 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 11 11:24:19 2023 +0200
@@ -224,11 +224,11 @@
 
 fun proof_syntax prf =
   let
-    val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
-      (fn PThm ({name, ...}, _) => if name <> "" then Symtab.update (name, ()) else I
-        | _ => I) [prf] Symtab.empty);
-    val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
-      (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
+    val thm_names = Symset.dest (Proofterm.fold_proof_atoms true
+      (fn PThm ({name, ...}, _) => if name <> "" then Symset.insert name else I
+        | _ => I) [prf] Symset.empty);
+    val axm_names = Symset.dest (Proofterm.fold_proof_atoms true
+      (fn PAxm (name, _, _) => Symset.insert name | _ => I) [prf] Symset.empty);
   in
     add_proof_syntax #>
     add_proof_atom_consts
diff -r d2645d3ad9e9 -r 15edec78869c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Apr 11 11:16:33 2023 +0200
+++ b/src/Pure/proofterm.ML	Tue Apr 11 11:24:19 2023 +0200
@@ -291,27 +291,27 @@
       | app (prf % _) = app prf
       | app (prf1 %% prf2) = app prf1 #> app prf2
       | app (prf as PThm ({serial = i, ...}, Thm_Body {body, ...})) = (fn (x, seen) =>
-          if Inttab.defined seen i then (x, seen)
+          if Intset.member seen i then (x, seen)
           else
             let val (x', seen') =
-              (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen)
+              (if all then app (join_proof body) else I) (x, Intset.insert i seen)
             in (f prf x', seen') end)
       | app prf = (fn (x, seen) => (f prf x, seen));
-  in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
+  in fn prfs => fn x => #1 (fold app prfs (x, Intset.empty)) end;
 
 fun fold_body_thms f =
   let
     fun app (PBody {thms, ...}) =
       tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
-        if Inttab.defined seen i then (x, seen)
+        if Intset.member seen i then (x, seen)
         else
           let
             val name = thm_node_name thm_node;
             val prop = thm_node_prop thm_node;
             val body = Future.join (thm_node_body thm_node);
-            val (x', seen') = app body (x, Inttab.update (i, ()) seen);
+            val (x', seen') = app body (x, Intset.insert i seen);
           in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
-  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
+  in fn bodies => fn x => #1 (fold app bodies (x, Intset.empty)) end;
 
 
 (* proof body *)
diff -r d2645d3ad9e9 -r 15edec78869c src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Tue Apr 11 11:16:33 2023 +0200
+++ b/src/Pure/thm_deps.ML	Tue Apr 11 11:24:19 2023 +0200
@@ -25,12 +25,12 @@
     fun collect (PBody {oracles, thms, ...}) =
       (if null oracles then I else apfst (cons oracles)) #>
       (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
-        if Inttab.defined seen i then (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, Inttab.update (i, ()) seen) end));
+          in collect body (res, Intset.insert i seen) end));
     val bodies = map Thm.proof_body_of thms;
-  in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end;
+  in fold collect bodies ([], Intset.empty) |> #1 |> Proofterm.unions_oracles end;
 
 fun has_skip_proof thms =
   all_oracles thms |> exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>);
@@ -112,17 +112,16 @@
 
     val used =
       Proofterm.fold_body_thms
-        (fn {name = a, ...} => a <> "" ? Symtab.update (a, ()))
+        (fn {name = a, ...} => a <> "" ? Symset.insert a)
         (map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
-        Symtab.empty;
+        Symset.empty;
 
-    fun is_unused a = not (Symtab.defined used a);
+    fun is_unused a = not (Symset.member used a);
 
     (*groups containing at least one used theorem*)
     val used_groups =
-      Inttab.build (new_thms |> fold (fn (a, (_, _, group)) =>
-        if is_unused a orelse group = 0 then I
-        else Inttab.update (group, ())));
+      Intset.build (new_thms |> fold (fn (a, (_, _, group)) =>
+        if is_unused a orelse group = 0 then I else Intset.insert group));
 
     val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
       if not concealed andalso
@@ -130,9 +129,9 @@
         Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a
       then
         (if group = 0 then ((a, th) :: thms, seen_groups)
-         else if Inttab.defined used_groups group orelse Inttab.defined seen_groups group then q
-         else ((a, th) :: thms, Inttab.update (group, ()) seen_groups))
-      else q) new_thms ([], Inttab.empty);
+         else if Intset.member used_groups group orelse Intset.member seen_groups group then q
+         else ((a, th) :: thms, Intset.insert group seen_groups))
+      else q) new_thms ([], Intset.empty);
   in rev thms' end;
 
 end;