--- a/IsaMakefile	Wed Dec 26 14:52:14 2012 +0000
+++ b/IsaMakefile	Wed Dec 26 19:03:06 2012 +0000
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d pdf  ## -D generated
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -D generated
 
 
 ## utm
@@ -22,18 +22,14 @@
 utm: $(OUT)/utm
 
 $(OUT)/utm: *.thy
-	@$(USEDIR) -b HOL UTM
+	@$(USEDIR) -f ROOT.ML -b HOL UTM
 
-session:  ROOT.ML \
+paper:  ROOT.ML \
 	document/root* \
 	*.thy
-	@$(USEDIR) -D generated -f ROOT.ML UTM .
-
-paper: utm
-	rm -f generated/*.aux # otherwise latex will fall over       
-	cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
-#	cd generated ; bibtex root
-#	cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+	rm -rf generated # otherwise latex will fall over 
+	@$(USEDIR) -f ROOT1.ML UTM .
+	$(ISABELLE_TOOL) document -o pdf  generated
 	cp generated/root.pdf paper.pdf