src/Pure/General/table.ML

--- a/src/Pure/General/table.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/General/table.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -19,6 +19,7 @@
   exception SAME
   exception UNDEF of key
   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
@@ -85,6 +86,8 @@
 
 val empty = Empty;
 
+fun build (f: 'a table -> 'a table) = f empty;
+
 fun is_empty Empty = true
   | is_empty _ = false;