--- a/IsaMakefile	Sun May 22 10:20:18 2011 +0200
+++ b/IsaMakefile	Tue May 24 19:39:38 2011 +0200
@@ -142,7 +142,7 @@
 session8: Slides/ROOT8.ML \
          Slides/document/root* \
          Slides/Slides6.thy
-	@$(USEDIR) -D generated8 -f ROOT8.ML HOL Slides
+	@$(USEDIR) -D generated8 -f ROOT8.ML HOL-Nominal Slides
 
 slides8: session8
 	rm -f Slides/generated8/*.aux # otherwise latex will fall over