# HG changeset patch
# User wenzelm
# Date 858853445 -3600
# Node ID 1262592be57969522ee32cb93cdde92a2f92e2d0
# Parent  50bac845de6f106dcab0307f95f740fd5e9d53df
isatool usedir;

diff -r 50bac845de6f -r 1262592be579 src/CTT/IsaMakefile
--- a/src/CTT/IsaMakefile	Thu Mar 20 11:23:19 1997 +0100
+++ b/src/CTT/IsaMakefile	Thu Mar 20 11:24:05 1997 +0100
@@ -12,14 +12,13 @@
 EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
 
 $(OUT)/CTT: $(OUT)/Pure $(FILES)
-	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure CTT
+	@$(ISATOOL) usedir -b $(OUT)/Pure CTT
 	@chmod -w $@
 
 $(OUT)/Pure:
 	@cd ../Pure; $(ISATOOL) make
 
 test: ex/ROOT.ML $(OUT)/CTT $(EX_FILES)
-	@$(ISABELLE) -e 'make_html := $(ISABELLE_HTML); exit_use"ex/ROOT.ML"; quit();' \
-	  -rq $(OUT)/CTT
+	@$(ISATOOL) usedir $(OUT)/CTT ex
 
 .PRECIOUS: $(OUT)/Pure $(OUT)/CTT
diff -r 50bac845de6f -r 1262592be579 src/FOLP/IsaMakefile
--- a/src/FOLP/IsaMakefile	Thu Mar 20 11:23:19 1997 +0100
+++ b/src/FOLP/IsaMakefile	Thu Mar 20 11:24:05 1997 +0100
@@ -14,13 +14,13 @@
 	   ex/prop.ML ex/quant.ML
 
 $(OUT)/FOLP: $(OUT)/Pure $(FILES)
-	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure FOLP
+	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
 	@chmod -w $@
 
 $(OUT)/Pure:
 	@cd ../Pure; $(ISATOOL) make
 
 test: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES)
-	@$(ISATOOL) testdir $(OUT)/FOLP ex
+	@$(ISATOOL) usedir $(OUT)/FOLP ex
 
 .PRECIOUS: $(OUT)/Pure $(OUT)/FOLP