Declares the function exit_use to behave like use but fail if
errors are detected. It can be used in all Makefiles except Pure, which will
write the exception handler explicitly ("exit" will have been declared
already).

--- a/src/Pure/library.ML	Wed Mar 15 10:53:58 1995 +0100
+++ b/src/Pure/library.ML	Wed Mar 15 10:56:39 1995 +0100
@@ -692,6 +692,8 @@
   (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
    writeln ("\n**** Finished " ^ fname ^ " ****")));
 
+(*For Makefiles: use the file, but exit with error code if errors found.*)
+fun exit_use fname = use fname handle _ => exit 1;
 
 
 (** filenames **)