# HG changeset patch
# User wenzelm
# Date 1395339891 -3600
# Node ID f61eaab6bec345b4f3ff387da9cee33f86e265e9
# Parent  0f6dc7512023496ee3a74dfc3be166ed3f14b9fd
tuned error, according to "use" in General/secure.ML;

diff -r 0f6dc7512023 -r f61eaab6bec3 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 20 15:38:49 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 19:24:51 2014 +0100
@@ -191,3 +191,7 @@
 
 end;
 
+fun use s =
+  ML_Context.eval_file true (Path.explode s)
+    handle ERROR msg => (writeln msg; error "ML error");
+
diff -r 0f6dc7512023 -r f61eaab6bec3 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 20 15:38:49 2014 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 20 19:24:51 2014 +0100
@@ -226,7 +226,6 @@
 (*ML with context and antiquotations*)
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
-val use = ML_Context.eval_file true o Path.explode;
 (*^^^^^ end of ML bootstrap 1 ^^^^^*)
 
 (*basic proof engine*)