# HG changeset patch
# User wenzelm
# Date 1190303296 -7200
# Node ID 015a8838e65670606ffe294e202306f089c6f705
# Parent  f79f6061525c5ec77bf9a1857c182f559668cdbd
improved error behaviour of use (bootstrap version);

diff -r f79f6061525c -r 015a8838e656 src/Pure/General/secure.ML
--- 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;