diff -r 5a32e6a78993 -r 55e2aef8909b doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Fri Jun 29 18:03:07 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Fri Jun 29 18:12:18 2001 +0200
@@ -154,7 +154,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/Typedef.thy \
+  Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedef.thy \
   Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
   Types/Overloading.thy Types/Axioms.thy
 	$(REALUSEDIR) Types