improved error behaviour of use (bootstrap version);

--- a/src/Pure/General/secure.ML	Thu Sep 20 16:37:34 2007 +0200
+++ b/src/Pure/General/secure.ML	Thu Sep 20 17:48:16 2007 +0200
@@ -70,6 +70,6 @@
 (*override previous toplevel bindings!*)
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
-val use = Secure.use;
+fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
 val execute = Secure.execute;
 val system = Secure.system;