# HG changeset patch
# User wenzelm
# Date 1680084356 -7200
# Node ID 1951f64707923c81a64e04d8f1d371ea229c58ab
# Parent  19c539f5d4d3e00bb9a139e34b419366e9ac7a92
discontinue somewhat pointless is_single, which also depends on details of internal data representation;

diff -r 19c539f5d4d3 -r 1951f6470792 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Wed Mar 29 12:02:34 2023 +0200
+++ b/src/Pure/General/set.ML	Wed Mar 29 12:05:56 2023 +0200
@@ -13,7 +13,6 @@
   val empty: T
   val build: (T -> T) -> T
   val is_empty: T -> bool
-  val is_single: T -> bool
   val fold: (elem -> 'a -> 'a) -> T -> 'a -> 'a
   val fold_rev: (elem -> 'a -> 'a) -> T -> 'a -> 'a
   val dest: T -> elem list
@@ -107,9 +106,6 @@
 fun is_empty Empty = true
   | is_empty _ = false;
 
-fun is_single (Leaf1 _) = true
-  | is_single _ = false;
-
 
 (* fold combinators *)
 
diff -r 19c539f5d4d3 -r 1951f6470792 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Mar 29 12:02:34 2023 +0200
+++ b/src/Pure/General/table.ML	Wed Mar 29 12:05:56 2023 +0200
@@ -22,7 +22,6 @@
   val empty: 'a table
   val build: ('a table -> 'a table) -> 'a table
   val is_empty: 'a table -> bool
-  val is_single: 'a table -> bool
   val map: (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
@@ -127,9 +126,6 @@
 fun is_empty Empty = true
   | is_empty _ = false;
 
-fun is_single (Leaf1 _) = true
-  | is_single _ = false;
-
 
 (* map and fold combinators *)
 
diff -r 19c539f5d4d3 -r 1951f6470792 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Mar 29 12:02:34 2023 +0200
+++ b/src/Pure/Syntax/parser.ML	Wed Mar 29 12:05:56 2023 +0200
@@ -46,7 +46,7 @@
 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;
+fun nts_is_unique (nts: nts) = Intset.size nts <= 1;
 
 
 (* tokens *)