diff -r be1bc3b88480 -r 0c248bed5225 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Sep 30 13:42:00 2001 +0200
+++ b/src/HOL/IsaMakefile	Mon Oct 01 11:56:40 2001 +0200
@@ -209,7 +209,7 @@
 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
-  Induct/LList.ML Induct/LList.thy Induct/Mutil.thy \
+  Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
   Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
   Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \