# 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;