--- a/src/HOL/ex/ROOT.ML Tue Nov 06 23:51:00 2001 +0100
+++ b/src/HOL/ex/ROOT.ML Tue Nov 06 23:51:16 2001 +0100
@@ -19,6 +19,7 @@
time_use_thy "MonoidGroup";
time_use_thy "Records";
+time_use_thy "Locales";
time_use_thy "StringEx";
time_use_thy "BinEx";