src/HOL/Lex/ROOT.ML
changeset 4907 0eb6730de30f
parent 4832 bc11b5b06f87
child 5323 028e00595280
--- a/src/HOL/Lex/ROOT.ML	Fri May 08 15:45:01 1998 +0200
+++ b/src/HOL/Lex/ROOT.ML	Fri May 08 18:33:29 1998 +0200
@@ -9,10 +9,10 @@
 use_thy"AutoChopper";
 use_thy"AutoChopper1";
 use_thy"AutoMaxChop";
-(* Do no swap the next 2.
+(* 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"NAe_of_RegExp";
-use_thy"Automata";
+use_thy"RegExp2NAe";
+use_thy"Scanner";