# HG changeset patch
# User wenzelm
# Date 942317931 -3600
# Node ID 69032a618aa94ba79484ed0f1d13628741a2667b
# Parent  29a7a79ee7f406db673962819edcc63af423f3da
with_path;

diff -r 29a7a79ee7f4 -r 69032a618aa9 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*)