src/Pure/ROOT.ML
changeset 60911 858694df711b
parent 60630 fc7625ec7427
child 60937 51425cbe8ce9
     1.1 --- a/src/Pure/ROOT.ML	Wed Aug 12 01:25:00 2015 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Aug 12 01:39:31 2015 +0200
     1.3 @@ -85,7 +85,15 @@
     1.4  use "General/change_table.ML";
     1.5  use "General/graph.ML";
     1.6  
     1.7 +
     1.8 +(* fundamental structures *)
     1.9 +
    1.10 +use "name.ML";
    1.11 +use "term.ML";
    1.12 +use "context.ML";
    1.13 +use "context_position.ML";
    1.14  use "System/options.ML";
    1.15 +use "config.ML";
    1.16  
    1.17  
    1.18  (* concurrency within the ML runtime *)
    1.19 @@ -132,15 +140,6 @@
    1.20  use "PIDE/active.ML";
    1.21  
    1.22  
    1.23 -(* fundamental structures *)
    1.24 -
    1.25 -use "name.ML";
    1.26 -use "term.ML";
    1.27 -use "context.ML";
    1.28 -use "context_position.ML";
    1.29 -use "config.ML";
    1.30 -
    1.31 -
    1.32  (* inner syntax *)
    1.33  
    1.34  use "Syntax/type_annotation.ML";