src/Pure/ROOT.ML
changeset 49560 11430dd89e35
parent 49041 9edfd36a0355
child 49561 26fc70e983c2
     1.1 --- a/src/Pure/ROOT.ML	Tue Sep 25 12:17:58 2012 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Sep 25 14:32:41 2012 +0200
     1.3 @@ -50,7 +50,6 @@
     1.4  use "General/same.ML";
     1.5  use "General/ord_list.ML";
     1.6  use "General/balanced_tree.ML";
     1.7 -use "General/graph.ML";
     1.8  use "General/linear_set.ML";
     1.9  use "General/buffer.ML";
    1.10  use "General/pretty.ML";
    1.11 @@ -66,6 +65,8 @@
    1.12  use "PIDE/xml.ML";
    1.13  use "PIDE/yxml.ML";
    1.14  
    1.15 +use "General/graph.ML";
    1.16 +
    1.17  
    1.18  (* concurrency within the ML runtime *)
    1.19