--- 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");
+
--- 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*)