diff -r 37e991068d96 -r 2c6167e2c587 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Nov 13 10:58:46 2007 +0100
+++ b/src/HOL/IsaMakefile	Tue Nov 13 10:59:26 2007 +0100
@@ -625,8 +625,9 @@
 HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
 
 $(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \
-  Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
-  Extraction/QuotRem.thy \
+  Extraction/Euclid.thy Extraction/Greatest_Common_Divisor.thy \
+  Extraction/Higman.thy Extraction/Pigeonhole.thy Extraction/QuotRem.thy \
+  Extraction/ROOT.ML Extraction/Util.thy \
   Extraction/Warshall.thy Extraction/document/root.tex \
   Extraction/document/root.bib
 	@$(ISATOOL) usedir $(OUT)/HOL Extraction