# HG changeset patch
# User wenzelm
# Date 1006539575 -3600
# Node ID 7bafe3d6c248194192cd45dd632e9ddc2c0bd5ea
# Parent  aa2b7b475a9444ee48b3db88ebfdf808137faf0f
time_use_thy "Locales";

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";