make LocalesTest last, because it sets funny flags;
authorwenzelm
Tue, 06 Sep 2005 16:59:52 +0200
changeset 17277 ab45d65bf204
parent 17276 3bb24e8b2cb2
child 17278 f27456a2a975
make LocalesTest last, because it sets funny flags;
src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Tue Sep 06 16:59:51 2005 +0200
+++ b/src/FOL/ex/ROOT.ML	Tue Sep 06 16:59:52 2005 +0200
@@ -13,8 +13,6 @@
 time_use     "foundn.ML";
 time_use_thy "Prolog";
 
-time_use_thy "LocaleTest";
-
 writeln"\n** Intuitionistic examples **\n";
 time_use_thy "Intuitionistic";
 
@@ -39,3 +37,6 @@
 
 writeln"\n** How to declare an oracle **\n";
 time_use_thy "IffOracle";
+
+(*regression test for locales -- sets several global flags!*)
+time_use_thy "LocaleTest";