diff -r e1c714d33c5c -r 5c6efec476ae src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Feb 26 11:21:29 2009 +0000
+++ b/src/HOL/IsaMakefile	Thu Feb 26 14:16:30 2009 +0100
@@ -13,7 +13,6 @@
   HOL-Library \
   HOL-ex \
   HOL-Auth \
-  HOL-AxClasses \
   HOL-Bali \
   HOL-Decision_Procs \
   HOL-Extraction \
@@ -796,15 +795,6 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
 
 
-## HOL-AxClasses
-
-HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
-
-$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy			\
-  AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
-
-
 ## HOL-Lattice
 
 HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
@@ -1068,22 +1058,22 @@
 ## clean
 
 clean:
-	@rm -f  $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL $(OUT)/HOL-Nominal $(OUT)/TLA \
-		$(LOG)/HOL.gz $(LOG)/TLA.gz \
-		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
-		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
-		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
-		$(LOG)/HOL-HoareParallel.gz \
-		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
-		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
-		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
-                $(LOG)/HOL-Bali.gz \
-		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
-                $(LOG)/HOL-Nominal-Examples.gz \
-		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
-		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
-		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
-                $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
-		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz \
-                $(OUT)/HOL-Word $(LOG)/HOL-Word.gz $(LOG)/HOL-Word-Examples.gz \
-                $(OUT)/HOL-NSA $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
+	@rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL		\
+		$(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz		\
+		$(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz		\
+		$(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz			\
+		$(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz			\
+		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz			\
+		$(LOG)/HOL-HoareParallel.gz $(LOG)/HOL-Lex.gz		\
+		$(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz		\
+		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz		\
+		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz			\
+		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz		\
+		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz	\
+		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix			\
+		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz	\
+		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz			\
+		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
+		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
+		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
+		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz