# HG changeset patch
# User wenzelm
# Date 1517324733 -3600
# Node ID f0b183b433cb836b1f22c7c70bef539c195d3c2a
# Parent  f0b2cc2ad4640750c5578107f6cc53b946f05b69
more operations;

diff -r f0b2cc2ad464 -r f0b183b433cb src/Pure/General/table.ML
--- 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 *)