--- a/src/HOL/GroupTheory/ROOT.ML Fri Sep 27 10:33:47 2002 +0200 +++ b/src/HOL/GroupTheory/ROOT.ML Fri Sep 27 10:34:05 2002 +0200 @@ -2,4 +2,4 @@ no_document use_thy "FuncSet"; use_thy "Sylow"; -use_thy "Ring"; +use_thy "Module";