diff -r 6ef9a9893fd6 -r 3ae9fe3c0f68 src/HOL/Subst/ROOT.ML
--- a/src/HOL/Subst/ROOT.ML	Wed Oct 04 13:11:57 1995 +0100
+++ b/src/HOL/Subst/ROOT.ML	Wed Oct 04 13:12:14 1995 +0100
@@ -1,4 +1,5 @@
-(*  Title: 	HOL/Subst
+(*  Title: 	HOL/Subst/ROOT.ML
+    ID:         $Id$
     Author: 	Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
@@ -26,12 +27,7 @@
 
 writeln"Root file for Substitutions and Unification";
 loadpath := ["Subst"];
-use_thy "Subst/Setplus";
 
-use_thy "Subst/AList";
-use_thy "Subst/UTerm";
-use_thy "Subst/UTLemmas";
+use_thy "Unifier";
 
-use_thy "Subst/Subst";
-use_thy "Subst/Unifier";
 writeln"END: Root file for Substitutions and Unification";