--- a/src/HOL/Lex/ROOT.ML Tue Nov 04 20:52:20 1997 +0100
+++ b/src/HOL/Lex/ROOT.ML Wed Nov 05 09:08:35 1997 +0100
@@ -7,3 +7,5 @@
HOL_build_completed; (*Make examples fail if HOL did*)
use_thy"AutoChopper";
+use_thy"AutoChopper1";
+use_thy"Regset_of_auto";