src/Pure/ROOT.ML
changeset 51947 3301612c4893
parent 51933 a60c6c90a447
child 51967 43fbd02eb9d0
--- a/src/Pure/ROOT.ML	Sun May 12 18:20:16 2013 +0200
+++ b/src/Pure/ROOT.ML	Sun May 12 18:22:44 2013 +0200
@@ -67,6 +67,8 @@
 
 use "General/graph.ML";
 
+use "System/options.ML";
+
 
 (* concurrency within the ML runtime *)
 
@@ -113,7 +115,6 @@
 use "context.ML";
 use "context_position.ML";
 use "config.ML";
-use "System/options.ML";
 
 
 (* inner syntax *)