# HG changeset patch
# User lcp
# Date 795261560 -3600
# Node ID cc929b9ddc80e3fc1a35dca14cad3c1eb2237954
# Parent  aa0c5f9daf5babdfec80d9328581cf4d6968ff81
Now calls exit_use instead of use, for prompt failure if errors are detected.

diff -r aa0c5f9daf5b -r cc929b9ddc80 src/ZF/Makefile
--- a/src/ZF/Makefile	Wed Mar 15 10:56:39 1995 +0100
+++ b/src/ZF/Makefile	Wed Mar 15 10:59:20 1995 +0100
@@ -35,8 +35,8 @@
 $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
-		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
-	sml*)	echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
+		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
+	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml; exit 1;;\
 	esac
@@ -59,7 +59,7 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
 
 IMP:   $(BIN)/ZF  $(IMP_FILES)
-	echo 'use"IMP/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
 
 ##Coinduction example
 COIND_THYS = Coind/ECR.thy Coind/Language.thy\
@@ -70,7 +70,7 @@
               $(COIND_THYS) $(COIND_THYS:.thy=.ML)
 
 Coind:  $(BIN)/ZF  $(COIND_FILES)
-	echo 'use"Coind/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use"Coind/ROOT.ML";quit();' | $(LOGIC)
 
 ##Miscellaneous examples
 EX_THYS = ex/Ramsey.thy ex/Integ.thy ex/twos_compl.thy ex/Bin.thy \
@@ -82,7 +82,7 @@
 
 #Test ZF by loading the examples in directory ex
 ex:     $(BIN)/ZF  $(EX_FILES)
-	echo 'use"ex/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
 
 #Full test.
 test:   $(BIN)/ZF IMP Coind ex