diff -r 18112403c809 -r cf947d1ec5ff src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Tue Mar 18 17:55:54 2003 +0100
+++ b/src/HOL/Algebra/ROOT.ML	Tue Mar 18 18:07:06 2003 +0100
@@ -6,3 +6,4 @@
 
 with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
 with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
+use_thy "Sylow";