# HG changeset patch
# User wenzelm
# Date 1701268194 -3600
# Node ID 01f9128ec65580072f23d35f827cc95aaf2c3abe
# Parent  238c4acdf984e4c82782e856bc4ea006ba387814
more compact representation;

diff -r 238c4acdf984 -r 01f9128ec655 src/Pure/General/bitset.ML
--- a/src/Pure/General/bitset.ML	Wed Nov 29 15:27:21 2023 +0100
+++ b/src/Pure/General/bitset.ML	Wed Nov 29 15:29:54 2023 +0100
@@ -18,6 +18,7 @@
   val fold: (elem -> 'a -> 'a) -> T -> 'a -> 'a
   val fold_rev: (elem -> 'a -> 'a) -> T -> 'a -> 'a
   val dest: T -> elem list
+  val is_unique: T -> bool
   val min: T -> elem option
   val max: T -> elem option
   val get_first: (elem -> 'a option) -> T -> 'a option
@@ -109,6 +110,10 @@
 
 val dest = Library.build o fold_rev_set cons;
 
+fun is_unique (set as Bitset t) =
+  is_empty set orelse
+  Inttab.size t = 1 andalso fold_set (fn _ => Integer.add 1) set 0 = 1;
+
 
 (* min/max entries *)
 
diff -r 238c4acdf984 -r 01f9128ec655 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Nov 29 15:27:21 2023 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Nov 29 15:29:54 2023 +0100
@@ -38,15 +38,15 @@
 fun tags_name (tags: tags) =
   the o Inttab.lookup (Inttab.build (Symtab.fold (Inttab.update_new o swap) tags));
 
-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) = Intset.size nts <= 1;
+type nts = Bitset.T;
+val nts_empty: nts = Bitset.empty;
+val nts_merge: nts * nts -> nts = Bitset.merge;
+fun nts_insert nt : nts -> nts = Bitset.insert nt;
+fun nts_member (nts: nts) = Bitset.member nts;
+fun nts_fold f (nts: nts) = Bitset.fold f nts;
+fun nts_subset (nts1: nts, nts2: nts) = Bitset.forall (nts_member nts2) nts1;
+fun nts_is_empty (nts: nts) = Bitset.is_empty nts;
+fun nts_is_unique (nts: nts) = Bitset.is_unique nts;
 
 
 (* tokens *)