diff -r cc3d971fe66a -r ca128c9100b6 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Sat Oct 20 22:07:44 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Sun Oct 21 19:35:40 2001 +0200
@@ -157,7 +157,7 @@
 HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz
 
 $(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \
-  Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedef.thy \
+  Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
 	$(REALUSEDIR) Types