minor performance tuning: more compact persistent data;

--- a/src/Pure/General/name_space.ML	Tue Apr 11 10:46:43 2023 +0200
+++ b/src/Pure/General/name_space.ML	Tue Apr 11 11:16:33 2023 +0200
@@ -11,7 +11,7 @@
 sig
   type entry =
    {concealed: bool,
-    group: serial option,
+    group: serial,
     theory_long_name: string,
     pos: Position.T,
     serial: serial}
@@ -108,7 +108,7 @@
 
 type entry =
  {concealed: bool,
-  group: serial option,
+  group: serial,
   theory_long_name: string,
   pos: Position.T,
   serial: serial};
@@ -329,7 +329,7 @@
  {scopes: Binding.scope list,
   restricted: (bool * Binding.scope) option,
   concealed: bool,
-  group: serial option,
+  group: serial,
   theory_long_name: string,
   path: (string * bool) list};
 
@@ -379,11 +379,11 @@
   map_naming (fn (scopes, restricted, concealed, group, _, path) =>
     (scopes, restricted, concealed, group, theory_long_name, path));
 
-fun get_group (Naming {group, ...}) = group;
+fun get_group (Naming {group, ...}) = if group = 0 then NONE else SOME group;
 
 fun set_group group =
   map_naming (fn (scopes, restricted, concealed, _, theory_long_name, path) =>
-    (scopes, restricted, concealed, group, theory_long_name, path));
+    (scopes, restricted, concealed, the_default 0 group, theory_long_name, path));
 
 fun new_group naming = set_group (SOME (serial ())) naming;
 val reset_group = set_group NONE;
@@ -405,7 +405,7 @@
 fun qualified_path mandatory binding = map_path (fn path =>
   path @ Binding.path_of (Binding.qualify_name mandatory binding ""));
 
-val global_naming = make_naming ([], NONE, false, NONE, "", []);
+val global_naming = make_naming ([], NONE, false, 0, "", []);
 val local_naming = global_naming |> add_path Long_Name.localN;
 
 

--- a/src/Pure/thm_deps.ML	Tue Apr 11 10:46:43 2023 +0200
+++ b/src/Pure/thm_deps.ML	Tue Apr 11 11:16:33 2023 +0200
@@ -121,23 +121,17 @@
     (*groups containing at least one used theorem*)
     val used_groups =
       Inttab.build (new_thms |> fold (fn (a, (_, _, group)) =>
-        if is_unused a then I
-        else
-          (case group of
-            NONE => I
-          | SOME grp => Inttab.update (grp, ()))));
+        if is_unused a orelse group = 0 then I
+        else Inttab.update (group, ())));
 
     val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) =>
       if not concealed andalso
         (* FIXME replace by robust treatment of thm groups *)
         Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a
       then
-        (case group of
-           NONE => ((a, th) :: thms, seen_groups)
-         | SOME grp =>
-             if Inttab.defined used_groups grp orelse
-               Inttab.defined seen_groups grp then q
-             else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
+        (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);
   in rev thms' end;