src/Pure/ROOT.ML
changeset 56203 76c72f4d0667
parent 56072 31e427387ab5
child 56205 ceb8a93460b7
     1.1 --- a/src/Pure/ROOT.ML	Tue Mar 18 12:25:17 2014 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Mar 18 13:36:28 2014 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  use "ML/ml_lex.ML";
     1.5  use "ML/ml_parse.ML";
     1.6  use "General/secure.ML";
     1.7 -(*^^^^^ end of basic ML bootstrap ^^^^^*)
     1.8 +(*^^^^^ end of ML bootstrap 0 ^^^^^*)
     1.9  use "General/integer.ML";
    1.10  use "General/stack.ML";
    1.11  use "General/queue.ML";
    1.12 @@ -222,7 +222,6 @@
    1.13  use "Isar/keyword.ML";
    1.14  use "Isar/parse.ML";
    1.15  use "Isar/args.ML";
    1.16 -use "ML/ml_context.ML";
    1.17  
    1.18  (*theory sources*)
    1.19  use "Thy/thy_header.ML";
    1.20 @@ -230,6 +229,11 @@
    1.21  use "Thy/html.ML";
    1.22  use "Thy/latex.ML";
    1.23  
    1.24 +(*ML with context and antiquotations*)
    1.25 +use "ML/ml_context.ML";
    1.26 +val use = ML_Context.eval_file true o Path.explode;
    1.27 +(*^^^^^ end of ML bootstrap 1 ^^^^^*)
    1.28 +
    1.29  (*basic proof engine*)
    1.30  use "Isar/proof_display.ML";
    1.31  use "Isar/attrib.ML";