diff -r 618247e82f3d -r e34b2265698a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Nov 06 22:50:38 2007 +0100
+++ b/src/HOL/IsaMakefile	Tue Nov 06 22:50:39 2007 +0100
@@ -9,7 +9,7 @@
 images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
         HOL-Word TLA HOL4
 
-#Note: keep targets sorted (except for HOL-Library)
+#Note: keep targets sorted (except for HOL-Library and HOL-ex)
 test: \
   HOL-Library \
   HOL-ex \
@@ -37,6 +37,7 @@
   HOL-NumberTheory \
   HOL-Prolog \
   HOL-SET-Protocol \
+  HOL-SizeChange \
   HOL-Statespace \
   HOL-Subst \
       TLA-Buffer \
@@ -513,10 +514,10 @@
 
 $(LOG)/HOL-SizeChange.gz: $(OUT)/HOL \
 	SizeChange/Kleene_Algebras.thy SizeChange/Graphs.thy \
-	SizeChange/Misc_Tools.thy SizeChange/Criterion \
-	SizeChange/Correctness SizeChange/Interpretation \
-	SizeChange/Implementation SizeChange/Size_Change_Termination \
-	SizeChange/Examples	SizeChange/sct.ML \
+	SizeChange/Misc_Tools.thy SizeChange/Criterion.thy \
+	SizeChange/Correctness.thy SizeChange/Interpretation.thy \
+	SizeChange/Implementation.thy SizeChange/Size_Change_Termination.thy \
+	SizeChange/Examples.thy	SizeChange/sct.ML \
 	SizeChange/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL SizeChange