--- a/src/HOL/Lex/ROOT.ML Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Lex/ROOT.ML Thu Mar 11 13:20:35 1999 +0100
@@ -4,8 +4,6 @@
Copyright 1998 TUM
*)
-HOL_build_completed; (*Make examples fail if HOL did*)
-
use_thy"AutoChopper";
use_thy"AutoChopper1";
use_thy"AutoMaxChop";