diff -r d10839c203bd -r 30ba169e8c45 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Sep 28 14:40:43 2008 +0200
+++ b/src/HOL/IsaMakefile	Sun Sep 28 14:46:51 2008 +0200
@@ -62,7 +62,7 @@
 
 ## HOL
 
-HOL: HOL-Plain $(OUT)/HOL
+HOL: Pure $(OUT)/HOL
 
 HOL-Plain: Pure $(OUT)/HOL-Plain