src/Pure/ROOT.ML
changeset 56203 76c72f4d0667
parent 56072 31e427387ab5
child 56205 ceb8a93460b7
--- a/src/Pure/ROOT.ML	Tue Mar 18 12:25:17 2014 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 18 13:36:28 2014 +0100
@@ -39,7 +39,7 @@
 use "ML/ml_lex.ML";
 use "ML/ml_parse.ML";
 use "General/secure.ML";
-(*^^^^^ end of basic ML bootstrap ^^^^^*)
+(*^^^^^ end of ML bootstrap 0 ^^^^^*)
 use "General/integer.ML";
 use "General/stack.ML";
 use "General/queue.ML";
@@ -222,7 +222,6 @@
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
 use "Isar/args.ML";
-use "ML/ml_context.ML";
 
 (*theory sources*)
 use "Thy/thy_header.ML";
@@ -230,6 +229,11 @@
 use "Thy/html.ML";
 use "Thy/latex.ML";
 
+(*ML with context and antiquotations*)
+use "ML/ml_context.ML";
+val use = ML_Context.eval_file true o Path.explode;
+(*^^^^^ end of ML bootstrap 1 ^^^^^*)
+
 (*basic proof engine*)
 use "Isar/proof_display.ML";
 use "Isar/attrib.ML";