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 *)