src/Pure/ROOT.ML
changeset 56205 ceb8a93460b7
parent 56203 76c72f4d0667
child 56206 7adec2a527f5
     1.1 --- a/src/Pure/ROOT.ML	Tue Mar 18 15:29:58 2014 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Mar 18 16:16:28 2014 +0100
     1.3 @@ -231,13 +231,13 @@
     1.4  
     1.5  (*ML with context and antiquotations*)
     1.6  use "ML/ml_context.ML";
     1.7 +use "ML/ml_antiquotation.ML";
     1.8  val use = ML_Context.eval_file true o Path.explode;
     1.9  (*^^^^^ end of ML bootstrap 1 ^^^^^*)
    1.10  
    1.11  (*basic proof engine*)
    1.12  use "Isar/proof_display.ML";
    1.13  use "Isar/attrib.ML";
    1.14 -use "ML/ml_antiquotation.ML";
    1.15  use "Isar/context_rules.ML";
    1.16  use "Isar/method.ML";
    1.17  use "Isar/proof.ML";