Now the "use" call has an exception handler, for prompt failure
if errors are detected.

--- a/src/Pure/Makefile	Wed Mar 15 10:34:47 1995 +0100
+++ b/src/Pure/Makefile	Wed Mar 15 10:53:58 1995 +0100
@@ -37,13 +37,13 @@
 	case "$(COMP)" in \
 	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
 		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
-		echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\
+		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' | $(COMP) $(BIN)/Pure;;\
 	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
            	then echo Bad value for ISABELLEBIN: \
                 	$(BIN) is not a writable directory; \
                 	exit 1; \
            	fi;\
-		echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\
+		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;'\
 			  | $(COMP);;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\