diff -r 710ddb9e8b5e -r 58ddb5049335 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Jan 20 00:01:40 2001 +0100
+++ b/src/HOL/IsaMakefile	Sat Jan 20 00:32:56 2001 +0100
@@ -178,7 +178,8 @@
 
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
   Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
-  Library/Quotient.thy Library/Ring_and_Field.thy Library/README.html \
+  Library/Quotient.thy Library/Ring_and_Field.thy \
+  Library/Ring_and_Field_Example.thy Library/README.html \
   Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \
   Library/While_Combinator.thy Library/While_Combinator_Example.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Library