use: tuned error;

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