diff -r e671abce8f8e -r a1b5357b5473 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Nov 29 11:54:12 2023 +0100
+++ b/src/Pure/context.ML	Wed Nov 29 13:01:03 2023 +0100
@@ -143,7 +143,7 @@
 abstype theory_id =
   Thy_Id of
    {id: id,         (*identifier*)
-    ids: Intset.T,  (*cumulative identifiers -- symbolic body content*)
+    ids: Bitset.T,  (*cumulative identifiers -- symbolic body content*)
     name: string,   (*official theory name*)
     stage: int}     (*index for anonymous updates*)
 with
@@ -338,13 +338,13 @@
 (* identity *)
 
 fun merge_ids thys =
-  fold (identity_of #> (fn {id, ids, ...} => fn acc => Intset.merge (acc, ids) |> Intset.insert id))
-    thys Intset.empty;
+  fold (identity_of #> (fn {id, ids, ...} => fn acc => Bitset.merge (acc, ids) |> Bitset.insert id))
+    thys Bitset.empty;
 
 val eq_thy_id = op = o apply2 (#id o rep_theory_id);
 val eq_thy = op = o apply2 (#id o identity_of);
 
-val proper_subthy_id = apply2 rep_theory_id #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id);
+val proper_subthy_id = apply2 rep_theory_id #> (fn ({id, ...}, {ids, ...}) => Bitset.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;
@@ -453,7 +453,7 @@
   let
     val state = make_state ();
     val stage = next_stage state;
-  in create_thy state Intset.empty PureN stage (make_ancestry [] []) Datatab.empty end;
+  in create_thy state Bitset.empty PureN stage (make_ancestry [] []) Datatab.empty end;
 
 local