src/HOL/Algebra/ROOT.ML

--- a/src/HOL/Algebra/ROOT.ML	Thu Nov 11 11:43:14 1999 +0100
+++ b/src/HOL/Algebra/ROOT.ML	Thu Nov 11 11:58:51 1999 +0100
@@ -4,8 +4,5 @@
     Author: Clemens Ballarin, started 24 September 1999
 *)
 
-add_path "abstract";
-add_path "poly";
-
-use_thy "Abstract";	(*The ring theory*)
-use_thy "Polynomial";	(*The full theory*)
+with_path "abstract" use_thy "Abstract";        (*The ring theory*)
+with_path "poly"     use_thy "Polynomial";      (*The full theory*)