diff -r aa2b7b475a94 -r 7bafe3d6c248 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Nov 23 17:19:14 2001 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Nov 23 19:19:35 2001 +0100
@@ -6,7 +6,7 @@
 
 time_use_thy "Recdefs";
 time_use_thy "Primrec";
-(* FIXME time_use_thy "Locales"; *)
+time_use_thy "Locales";
 time_use_thy "Records";
 time_use_thy "MonoidGroup";
 time_use_thy "StringEx";