--- a/src/HOL/ROOT.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/ROOT.ML Wed Oct 04 13:10:03 1995 +0100
@@ -1,4 +1,4 @@
-(* Title: CHOL/ROOT.ML
+(* Title: HOL/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1993 University of Cambridge
@@ -18,7 +18,6 @@
use "thy_syntax.ML";
use_thy "HOL";
-use "../Provers/simplifier.ML";
use "../Provers/splitter.ML";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";
@@ -64,7 +63,6 @@
use "simpdata.ML";
use_thy "Ord";
use_thy "subset";
-use_thy "equalities";
use "hologic.ML";
use "subtype.ML";
use_thy "Prod";