diff -r b11d7ffb48e0 -r a9df6686ed0e src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Apr 29 15:16:17 2020 +0100
+++ b/src/HOL/ROOT	Mon May 04 16:28:39 2020 +0200
@@ -240,6 +240,7 @@
     Tree_Map
     Interval_Tree
     AVL_Map
+    AVL_Bal_Set
     Height_Balanced_Tree
     RBT_Set2
     RBT_Map