# HG changeset patch
# User wenzelm
# Date 1679946527 -7200
# Node ID b761c91c2447daf0758db5559bee97dda79faac5
# Parent  8faf28a80a7fc66bf5afc99a86aa04546fb5d8e1
performance tuning: prefer functor Set() over Table();

diff -r 8faf28a80a7f -r b761c91c2447 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -42,7 +42,7 @@
   val get_quotients           : Proof.context -> quotient Symtab.table
   val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
   val get_restore_data        : Proof.context -> restore_data Symtab.table
-  val get_no_code_types       : Proof.context -> unit Symtab.table
+  val get_no_code_types       : Proof.context -> Symset.T
 end
 
 structure Lifting_Info: LIFTING_INFO =
@@ -82,7 +82,7 @@
       reflexivity_rules : thm Item_Net.T,
       relator_distr_data : relator_distr_data Symtab.table,
       restore_data : restore_data Symtab.table,
-      no_code_types : unit Symtab.table
+      no_code_types : Symset.T
     }
   val empty =
     { quot_maps = Symtab.empty,
@@ -90,7 +90,7 @@
       reflexivity_rules = Thm.item_net,
       relator_distr_data = Symtab.empty,
       restore_data = Symtab.empty,
-      no_code_types = Symtab.empty
+      no_code_types = Symset.empty
     }
   fun merge
     ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1,
@@ -102,7 +102,7 @@
       reflexivity_rules = Item_Net.merge (rr1, rr2),
       relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
       restore_data = Symtab.join join_restore_data (rd1, rd2),
-      no_code_types = Symtab.merge (K true) (nct1, nct2)
+      no_code_types = Symset.merge (nct1, nct2)
     }
 )
 
@@ -543,9 +543,9 @@
 (* no_code types *)
 
 fun add_no_code_type type_name context =
-  Data.map (map_no_code_types (Symtab.update (type_name, ()))) context;
+  Data.map (map_no_code_types (Symset.insert type_name)) context;
 
-fun is_no_code_type context type_name = (Symtab.defined o get_no_code_types) context type_name
+fun is_no_code_type context type_name = (Symset.member o get_no_code_types) context type_name
 
 
 (* setup fixed eq_onp rules *)
diff -r 8faf28a80a7f -r b761c91c2447 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -48,15 +48,15 @@
         (case String.tokens (fn c => c = #".") name of
           [name] => (("", name, args), labels)
         | [label, name] =>
-          (if Symtab.defined labels label then
+          (if Symset.member labels label then
              error ("Action label '" ^ label ^ "' already defined.")
            else
              ();
-           ((label, name, args), Symtab.insert_set label labels))
+           ((label, name, args), Symset.insert label labels))
         | _ => error "Cannot parse action")
   in
     try read_actions ()
-    |> Option.map (fn xs => fst (fold_map split_name_label xs Symtab.empty))
+    |> Option.map (fn xs => fst (fold_map split_name_label xs Symset.empty))
   end
 
 
diff -r 8faf28a80a7f -r b761c91c2447 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -27,18 +27,18 @@
 structure Data = Theory_Data
 (
   type T =
-    {ignore_consts : unit Symtab.table,
-     keep_functions : unit Symtab.table,
+    {ignore_consts : Symset.T,
+     keep_functions : Symset.T,
      processed_specs : ((string * thm list) list) Symtab.table};
   val empty =
-    {ignore_consts = Symtab.empty,
-     keep_functions = Symtab.empty,
+    {ignore_consts = Symset.empty,
+     keep_functions = Symset.empty,
      processed_specs =  Symtab.empty};
   fun merge
     ({ignore_consts = c1, keep_functions = k1, processed_specs = s1},
      {ignore_consts = c2, keep_functions = k2, processed_specs = s2}) =
-     {ignore_consts = Symtab.merge (K true) (c1, c2),
-      keep_functions = Symtab.merge (K true) (k1, k2),
+     {ignore_consts = Symset.merge (c1, c2),
+      keep_functions = Symset.merge (k1, k2),
       processed_specs = Symtab.merge (K true) (s1, s2)}
 );
 
@@ -48,12 +48,12 @@
 fun map_data f {ignore_consts = c, keep_functions = k, processed_specs = s} = mk_data (f (c, k, s))
 
 fun ignore_consts cs =
-  Data.map (map_data (@{apply 3(1)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+  Data.map (map_data (@{apply 3(1)} (fold Symset.insert cs)))
 
 fun keep_functions cs =
-  Data.map (map_data (@{apply 3(2)} (fold (fn c => Symtab.insert (op =) (c, ())) cs)))
+  Data.map (map_data (@{apply 3(2)} (fold Symset.insert cs)))
 
-fun keep_function thy = Symtab.defined (#keep_functions (Data.get thy))
+fun keep_function thy = Symset.member (#keep_functions (Data.get thy))
 
 fun processed_specs thy = Symtab.lookup (#processed_specs (Data.get thy))
 
@@ -274,7 +274,7 @@
       |> filter_out has_code_pred_intros
       |> filter_out case_consts
       |> filter_out special_cases
-      |> filter_out (fn (c, _) => Symtab.defined (#ignore_consts (Data.get thy)) c)
+      |> filter_out (fn (c, _) => Symset.member (#ignore_consts (Data.get thy)) c)
       |> map (fn (c, _) => (c, Sign.the_const_constraint thy c))
       |> map Const
       (*
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -181,7 +181,7 @@
 
 end;
 
-structure Tasks = Table(type key = task val ord = task_ord);
+structure Tasks = Set(type key = task val ord = task_ord);
 structure Task_Graph = Graph(type key = task val ord = task_ord);
 
 
@@ -205,16 +205,16 @@
 
 (* known group members *)
 
-type groups = unit Tasks.table Inttab.table;
+type groups = Tasks.T Inttab.table;
 
 fun get_tasks (groups: groups) gid =
   the_default Tasks.empty (Inttab.lookup groups gid);
 
 fun add_task (gid, task) groups =
-  Inttab.update (gid, Tasks.update (task, ()) (get_tasks groups gid)) groups;
+  Inttab.update (gid, Tasks.insert task (get_tasks groups gid)) groups;
 
 fun del_task (gid, task) groups =
-  let val tasks = Tasks.delete_safe task (get_tasks groups gid) in
+  let val tasks = Tasks.remove task (get_tasks groups gid) in
     if Tasks.is_empty tasks then Inttab.delete_safe gid groups
     else Inttab.update (gid, tasks) groups
   end;
@@ -246,9 +246,9 @@
 val empty = make_queue Inttab.empty Task_Graph.empty 0 0;
 
 fun group_tasks (Queue {groups, ...}) gs =
-  fold (fn g => fn tasks => Tasks.merge (op =) (tasks, get_tasks groups (group_id g)))
+  fold (fn g => fn tasks => Tasks.merge (tasks, get_tasks groups (group_id g)))
     gs Tasks.empty
-  |> Tasks.keys;
+  |> Tasks.dest;
 
 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
 
@@ -298,7 +298,7 @@
   let
     val _ = cancel_group group Exn.Interrupt;
     val running =
-      Tasks.fold (fn (task, _) =>
+      Tasks.fold (fn task =>
           (case get_job jobs task of Running thread => insert Thread.equal thread | _ => I))
         (get_tasks groups (group_id group)) [];
   in running end;
@@ -405,11 +405,11 @@
 
     fun ready_dep _ [] = NONE
       | ready_dep seen (task :: tasks) =
-          if Tasks.defined seen task then ready_dep seen tasks
+          if Tasks.member seen task then ready_dep seen tasks
           else
             let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
               (case ready_job (task, entry) of
-                NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks)
+                NONE => ready_dep (Tasks.insert task seen) (Task_Graph.Keys.dest ds @ tasks)
               | some => some)
             end;
 
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/General/change_table.ML
--- a/src/Pure/General/change_table.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/General/change_table.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -36,6 +36,7 @@
 struct
 
 structure Table = Table(Key);
+structure Set = Set(Key);
 type key = Table.key;
 
 exception SAME = Table.SAME;
@@ -45,7 +46,7 @@
 (* optional change *)
 
 datatype change =
-  No_Change | Change of {base: serial, depth: int, changes: Table.set option};
+  No_Change | Change of {base: serial, depth: int, changes: Set.T option};
 
 fun make_change base depth changes =
   Change {base = base, depth = depth, changes = changes};
@@ -55,11 +56,11 @@
   | ignore_change change = change;
 
 fun update_change key (Change {base, depth, changes = SOME ch}) =
-      make_change base depth (SOME (Table.insert (K true) (key, ()) ch))
+      make_change base depth (SOME (Set.insert key ch))
   | update_change _ change = change;
 
 fun base_change true No_Change =
-      make_change (serial ()) 0 (SOME Table.empty)
+      make_change (serial ()) 0 (SOME Set.empty)
   | base_change true (Change {base, depth, changes}) =
       make_change base (depth + 1) changes
   | base_change false (Change {base, depth, changes}) =
@@ -128,7 +129,7 @@
                       (case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of
                         NONE => tab
                       | SOME z => Table.update (key, z) tab)));
-          in make_change_table (change', Table.fold (update o #1) ch2 tab1) end)
+          in make_change_table (change', Set.fold update ch2 tab1) end)
   end;
 
 fun merge eq =
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/General/graph.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -76,22 +76,23 @@
 val eq_key = is_equal o Key.ord;
 
 structure Table = Table(Key);
+structure Set = Set(Key);
 
 structure Keys =
 struct
 
-abstype T = Keys of unit Table.table
+abstype T = Keys of Set.T
 with
 
-val empty = Keys Table.empty;
-fun is_empty (Keys tab) = Table.is_empty tab;
+val empty = Keys Set.empty;
+fun is_empty (Keys set) = Set.is_empty set;
 
-fun member (Keys tab) = Table.defined tab;
-fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
-fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
+fun member (Keys set) = Set.member set;
+fun insert x (Keys set) = Keys (Set.insert x set);
+fun remove x (Keys set) = Keys (Set.remove x set);
 
-fun fold f (Keys tab) = Table.fold (f o #1) tab;
-fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
+fun fold f (Keys set) = Set.fold f set;
+fun fold_rev f (Keys set) = Set.fold_rev f set;
 
 fun dest keys = fold_rev cons keys [];
 
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/General/symbol.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -246,7 +246,7 @@
 
 local
   val letter_symbols =
-    Symtab.make_set [
+    Symset.make [
       "\<A>",
       "\<B>",
       "\<C>",
@@ -388,7 +388,7 @@
     ];
 in
 
-val is_letter_symbol = Symtab.defined letter_symbols;
+val is_letter_symbol = Symset.member letter_symbols;
 
 end;
 
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/Isar/experiment.ML
--- a/src/Pure/Isar/experiment.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Isar/experiment.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -16,12 +16,12 @@
 
 structure Data = Theory_Data
 (
-  type T = Symtab.set;
-  val empty = Symtab.empty;
-  val merge = Symtab.merge (K true);
+  type T = Symset.T;
+  val empty = Symset.empty;
+  val merge = Symset.merge;
 );
 
-fun is_experiment thy name = Symtab.defined (Data.get thy) name;
+fun is_experiment thy name = Symset.member (Data.get thy) name;
 
 fun gen_experiment add_locale elems thy =
   let
@@ -29,7 +29,7 @@
     val lthy =
       thy
       |> add_locale experiment_name Binding.empty [] ([], []) elems
-      |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set);
+      |-> (Local_Theory.background_theory o Data.map o Symset.insert);
     val (scope, naming) =
       Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
     val naming' = naming |> Name_Space.private_scope scope;
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Isar/keyword.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -242,11 +242,11 @@
 
 fun command_category ks =
   let
-    val tab = Symtab.make_set ks;
+    val set = Symset.make ks;
     fun pred keywords name =
       (case lookup_command keywords name of
         NONE => false
-      | SOME {kind, ...} => Symtab.defined tab kind);
+      | SOME {kind, ...} => Symset.member set kind);
   in pred end;
 
 val is_vacuous = command_category [diag, document_heading, document_body, document_raw];
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -1285,17 +1285,17 @@
     val serial_of = #serial oo (Name_Space.the_entry o Name_Space.space_of_table);
     val ignored =
       (case prev_ctxt of
-        NONE => Inttab.empty
+        NONE => Intset.empty
       | SOME ctxt0 =>
           let val cases0 = cases_of ctxt0 in
-            Inttab.build (cases0 |> Name_Space.fold_table (fn (a, _) =>
-              Inttab.insert_set (serial_of cases0 a)))
+            Intset.build (cases0 |> Name_Space.fold_table (fn (a, _) =>
+              Intset.insert (serial_of cases0 a)))
           end);
      val cases = cases_of ctxt;
   in
     Name_Space.fold_table (fn (a, c) =>
       let val i = serial_of cases a
-      in not (Inttab.defined ignored i) ? cons (i, (a, c)) end) cases []
+      in not (Intset.member ignored i) ? cons (i, (a, c)) end) cases []
     |> sort (int_ord o apply2 #1) |> map #2
   end;
 
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -54,7 +54,7 @@
 
 type perspective =
  {required: bool,  (*required node*)
-  visible: Inttab.set,  (*visible commands*)
+  visible: Intset.T,  (*visible commands*)
   visible_last: Document_ID.command option,  (*last visible command*)
   overlays: (string * string list) list Inttab.table};  (*command id -> print functions with args*)
 
@@ -79,7 +79,7 @@
 
 fun make_perspective (required, command_ids, overlays) : perspective =
  {required = required,
-  visible = Inttab.make_set command_ids,
+  visible = Intset.make command_ids,
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
@@ -93,7 +93,7 @@
 
 fun is_empty_perspective ({required, visible, visible_last, overlays}: perspective) =
   not required andalso
-  Inttab.is_empty visible andalso
+  Intset.is_empty visible andalso
   is_none visible_last andalso
   Inttab.is_empty overlays;
 
@@ -147,7 +147,7 @@
 
 val required_node = #required o get_perspective;
 val command_overlays = Inttab.lookup_list o #overlays o get_perspective;
-val command_visible = Inttab.defined o #visible o get_perspective;
+val command_visible = Intset.member o #visible o get_perspective;
 val visible_last = #visible_last o get_perspective;
 val visible_node = is_some o visible_last
 
@@ -516,14 +516,14 @@
     fun all_preds P =
       String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes []
       |> String_Graph.all_preds nodes
-      |> Symtab.make_set;
+      |> Symset.make;
 
     val all_visible = all_preds visible_node;
     val all_required = all_preds required_node;
   in
-    Symtab.fold (fn (a, ()) =>
-      exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
-        Symtab.update (a, ())) all_visible all_required
+    Symset.fold (fn a =>
+      exists (Symset.member all_visible) (String_Graph.immediate_succs nodes a) ?
+        Symset.insert a) all_visible all_required
   end;
 
 fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
@@ -548,7 +548,7 @@
       val _ =
         nodes |> String_Graph.schedule
           (fn deps => fn (name, node) =>
-            if Symtab.defined required name orelse visible_node node orelse pending_result node then
+            if Symset.member required name orelse visible_node node orelse pending_result node then
               let
                 val future =
                   (singleton o Future.forks)
@@ -812,11 +812,11 @@
       timeit "Document.edit_nodes"
         (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
 
-    val consolidate = Symtab.defined (Symtab.make_set consolidate);
+    val consolidate = Symset.member (Symset.make consolidate);
     val nodes = nodes_of new_version;
     val required = make_required nodes;
     val required0 = make_required (nodes_of old_version);
-    val edited = Symtab.build (edits |> fold (Symtab.insert_set o #1));
+    val edited = Symset.build (edits |> fold (Symset.insert o #1));
 
     val updated = timeit "Document.update" (fn () =>
       nodes |> String_Graph.schedule
@@ -834,11 +834,11 @@
                     val maybe_consolidate = consolidate name andalso could_consolidate node;
                     val imports = map (apsnd Future.join) deps;
                     val imports_result_changed = exists (#4 o #1 o #2) imports;
-                    val node_required = Symtab.defined required name;
+                    val node_required = Symset.member required name;
                   in
-                    if Symtab.defined edited name orelse maybe_consolidate orelse
+                    if Symset.member edited name orelse maybe_consolidate orelse
                       visible_node node orelse imports_result_changed orelse
-                      Symtab.defined required0 name <> node_required
+                      Symset.member required0 name <> node_required
                     then
                       let
                         val node0 = node_of old_version name;
@@ -906,7 +906,7 @@
     val state' = state
       |> define_version new_version_id new_version assigned_nodes;
 
-  in (Symtab.keys edited, removed, assign_result, state') end);
+  in (Symset.dest edited, removed, assign_result, state') end);
 
 end;
 
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/PIDE/resources.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -107,7 +107,7 @@
     load_commands = []: (string * Position.T) list,
     scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table},
    {global_theories = Symtab.empty: string Symtab.table,
-    loaded_theories = Symtab.empty: unit Symtab.table});
+    loaded_theories = Symset.empty: Symset.T});
 
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
@@ -125,7 +125,7 @@
         load_commands = load_commands,
         scala_functions = Symtab.make scala_functions},
        {global_theories = Symtab.make global_theories,
-        loaded_theories = Symtab.make_set loaded_theories}));
+        loaded_theories = Symset.make loaded_theories}));
 
 fun init_session_yxml yxml =
   let
@@ -169,7 +169,7 @@
 fun get_session_base2 f = get_session_base (f o #2);
 
 fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a;
-fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a;
+fun loaded_theory a = Symset.member (get_session_base2 #loaded_theories) a;
 
 fun check_session ctxt arg =
   Completion.check_item "session"
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -38,15 +38,15 @@
 fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
 fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
 
-type nts = Inttab.set;
-val nts_empty: nts = Inttab.empty;
-val nts_merge: nts * nts -> nts = Inttab.merge (K true);
-fun nts_insert nt : nts -> nts = Inttab.insert_set nt;
-fun nts_member (nts: nts) = Inttab.defined nts;
-fun nts_fold f (nts: nts) = Inttab.fold (f o #1) nts;
-fun nts_subset (nts1: nts, nts2: nts) = Inttab.forall (nts_member nts2 o #1) nts1;
-fun nts_is_empty (nts: nts) = Inttab.is_empty nts;
-fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Inttab.is_single nts;
+type nts = Intset.T;
+val nts_empty: nts = Intset.empty;
+val nts_merge: nts * nts -> nts = Intset.merge;
+fun nts_insert nt : nts -> nts = Intset.insert nt;
+fun nts_member (nts: nts) = Intset.member nts;
+fun nts_fold f (nts: nts) = Intset.fold f nts;
+fun nts_subset (nts1: nts, nts2: nts) = Intset.forall (nts_member nts2) nts1;
+fun nts_is_empty (nts: nts) = Intset.is_empty nts;
+fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Intset.is_single nts;
 
 
 (* tokens *)
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/context.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -127,7 +127,7 @@
   Theory_Id of
    (*identity*)
    {id: serial,                   (*identifier*)
-    ids: Inttab.set} *            (*cumulative identifiers -- symbolic body content*)
+    ids: Intset.T} *              (*cumulative identifiers -- symbolic body content*)
    (*history*)
    {name: string,                 (*official theory name*)
     stage: stage option}          (*index and counter for anonymous updates*)
@@ -215,14 +215,12 @@
 
 (* build ids *)
 
-fun insert_id id ids = Inttab.update (id, ()) ids;
-
 val merge_ids =
   apply2 (theory_id #> rep_theory_id #> #1) #>
   (fn ({id = id1, ids = ids1, ...}, {id = id2, ids = ids2, ...}) =>
-    Inttab.merge (K true) (ids1, ids2)
-    |> insert_id id1
-    |> insert_id id2);
+    Intset.merge (ids1, ids2)
+    |> Intset.insert id1
+    |> Intset.insert id2);
 
 
 (* equality and inclusion *)
@@ -231,7 +229,7 @@
 val eq_thy = op = o apply2 (#id o identity_of);
 
 val proper_subthy_id =
-  apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Inttab.defined ids id);
+  apply2 (rep_theory_id #> #1) #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id);
 val proper_subthy = proper_subthy_id o apply2 theory_id;
 
 fun subthy_id p = eq_thy_id p orelse proper_subthy_id p;
@@ -345,7 +343,7 @@
 (* primitives *)
 
 val pre_pure_thy =
-  create_thy Inttab.empty (make_history PureN) (make_ancestry [] []) Datatab.empty;
+  create_thy Intset.empty (make_history PureN) (make_ancestry [] []) Datatab.empty;
 
 local
 
@@ -358,7 +356,7 @@
       then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))
       else ancestry;
     val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage};
-    val ids' = insert_id id ids;
+    val ids' = Intset.insert id ids;
     val data' = f data;
   in create_thy ids' history' ancestry' data' end;
 
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/more_thm.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -253,8 +253,8 @@
 
 structure Hyps = Proof_Data
 (
-  type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T};
-  fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []};
+  type T = {checked_hyps: bool, hyps: Termset.T, shyps: sort Ord_List.T};
+  fun init _ : T = {checked_hyps = true, hyps = Termset.empty, shyps = []};
 );
 
 fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} =>
@@ -267,7 +267,7 @@
 fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) =>
   let
     val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct;
-    val hyps' = Termtab.update (Thm.term_of ct, ()) hyps;
+    val hyps' = Termset.insert (Thm.term_of ct) hyps;
   in (checked_hyps, hyps', shyps) end);
 
 fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt);
@@ -285,7 +285,7 @@
     | Context.Proof ctxt =>
         (case Hyps.get ctxt of
           {checked_hyps = false, ...} => K true
-        | {hyps, ...} => Termtab.defined hyps));
+        | {hyps, ...} => Termset.member hyps));
 
 fun check_hyps context th =
   (case undeclared_hyps context th of
diff -r 8faf28a80a7f -r b761c91c2447 src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Mon Mar 27 19:41:18 2023 +0200
+++ b/src/Pure/term_ord.ML	Mon Mar 27 21:48:47 2023 +0200
@@ -219,6 +219,9 @@
   fun term_cache f = Cache.create empty lookup update f;
 end;
 
+structure Sortset = Set(type key = sort val ord = Term_Ord.sort_ord);
+structure Termset = Set(type key = term val ord = Term_Ord.fast_term_ord);
+
 structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
 structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
 structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);