src/HOL/Lex/ROOT.ML

--- a/src/HOL/Lex/ROOT.ML	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/ROOT.ML	Tue Apr 18 00:36:02 2000 +0200
@@ -7,11 +7,5 @@
 use_thy"AutoChopper";
 use_thy"AutoChopper1";
 use_thy"AutoMaxChop";
-(* Do not swap the next two use_thy's.
-   There is some interference, probably via claset() or simpset().
-   Or via ML-bound names of axioms that are overwritten?
-*)
 use_thy"RegSet_of_nat_DA";
-use_thy"RegExp2NA";
-use_thy"RegExp2NAe";
 use_thy"Scanner";