src/Pure/ROOT.ML
changeset 60911 858694df711b
parent 60630 fc7625ec7427
child 60937 51425cbe8ce9
--- a/src/Pure/ROOT.ML	Wed Aug 12 01:25:00 2015 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 12 01:39:31 2015 +0200
@@ -85,7 +85,15 @@
 use "General/change_table.ML";
 use "General/graph.ML";
 
+
+(* fundamental structures *)
+
+use "name.ML";
+use "term.ML";
+use "context.ML";
+use "context_position.ML";
 use "System/options.ML";
+use "config.ML";
 
 
 (* concurrency within the ML runtime *)
@@ -132,15 +140,6 @@
 use "PIDE/active.ML";
 
 
-(* fundamental structures *)
-
-use "name.ML";
-use "term.ML";
-use "context.ML";
-use "context_position.ML";
-use "config.ML";
-
-
 (* inner syntax *)
 
 use "Syntax/type_annotation.ML";