| changeset 31473 | fd341ca4b8de |
| parent 31330 | 7bfbd0e07a40 |
| child 32738 | 15bb09ca0378 |
--- a/src/Pure/General/secure.ML Sat Jun 06 19:58:10 2009 +0200 +++ b/src/Pure/General/secure.ML Sat Jun 06 19:58:10 2009 +0200 @@ -70,7 +70,7 @@ val use_text = Secure.use_text; val use_file = Secure.use_file; fun use s = Secure.use_file ML_Parse.global_context true s - handle ERROR msg => (writeln msg; raise Fail "ML error"); + handle ERROR msg => (writeln msg; error "ML error"); val toplevel_pp = Secure.toplevel_pp; val system_out = Secure.system_out; val system = Secure.system;