diff -r ee3d40b5ac23 -r e88c2c89f98e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jul 02 21:53:11 2001 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 03 15:28:24 2001 +0200
@@ -259,8 +259,11 @@
 
 $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
   Library/Primes.thy \
-  GroupTheory/Exponent.thy GroupTheory/Exponent.ML GroupTheory/Group.thy\
-  GroupTheory/Group.ML GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
+  GroupTheory/Exponent.thy GroupTheory/Exponent.ML\
+  GroupTheory/Coset.thy GroupTheory/Coset.ML\
+  GroupTheory/DirProd.thy GroupTheory/DirProd.ML\
+  GroupTheory/Group.thy GroupTheory/Group.ML\
+  GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
   GroupTheory/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL GroupTheory