diff -r 9b673588244a -r a9b6a00b1ba0 IsaMakefile
--- a/IsaMakefile	Sat Sep 18 05:13:42 2010 +0800
+++ b/IsaMakefile	Sat Sep 18 06:09:43 2010 +0800
@@ -20,15 +20,15 @@
 
 tests: $(LOG)/HOL-Nominal2.gz
 
-$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
-	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
+#$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
+#	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
 
 ## Nominal2 Paper
 
 paper: $(LOG)/HOL-Nominal2-Paper.gz
 
 $(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy
-	@$(USEDIR) -D generated Nominal Paper
+	@$(USEDIR) -D generated HOL Paper
 	$(ISABELLE_TOOL) document -o pdf  Paper/generated
 	@cp Paper/document.pdf paper.pdf