# HG changeset patch
# User wenzelm
# Date 1244311090 -7200
# Node ID fd341ca4b8deb9320d556cbcfd2638a5aa99c401
# Parent  d7929d74acb42c4bd3cb8000ed22432a48285f5b
use: tuned error;

diff -r d7929d74acb4 -r fd341ca4b8de src/Pure/General/secure.ML
--- 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;