diff -r 2f45f4abf0a9 -r 70643edecb7a src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/ROOT	Mon Jun 05 15:59:45 2017 +0200
@@ -52,6 +52,8 @@
     DAList_Multiset
     RBT_Mapping
     RBT_Set
+    (*printing modifications*)
+    OptionalSugar
     (*prototypic tools*)
     Predicate_Compile_Quickcheck
     (*legacy tools*)