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 *)