| changeset 24663 | 015a8838e656 |
| parent 24600 | 5877b88f262c |
| child 24858 | a3a81e73f552 |
--- 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;