--- a/src/Pure/General/table.ML Tue Jan 30 15:40:01 2018 +0100
+++ b/src/Pure/General/table.ML Tue Jan 30 16:05:33 2018 +0100
@@ -20,6 +20,7 @@
exception UNDEF of key
val empty: '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
@@ -77,13 +78,16 @@
exception DUP of key;
-(* empty *)
+(* empty and single *)
val empty = Empty;
fun is_empty Empty = true
| is_empty _ = false;
+fun is_single (Branch2 (Empty, _, Empty)) = true
+ | is_single _ = false;
+
(* map and fold combinators *)