diff -r 499637e8f2c6 -r 0376cccd9118 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Wed Oct 11 09:09:06 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Wed Oct 11 10:44:42 2000 +0200
@@ -89,7 +89,7 @@
 
 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \
   Recdef/simplification.thy Recdef/Induction.thy \
-  Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy Recdef/WFrec.thy
+  Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
 	@rm -f tutorial.dvi
 
@@ -98,7 +98,7 @@
 
 HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
 
-$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
+$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy
 	@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Advanced
 	@rm -f tutorial.dvi