diff -r 52c7bcfc9515 -r 3f2a6c66e089 src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Sat Jul 07 00:14:49 2007 +0200 +++ b/src/Pure/General/ROOT.ML Sat Jul 07 00:14:52 2007 +0200 @@ -8,9 +8,9 @@ use "ord_list.ML"; use "alist.ML"; use "table.ML"; +use "graph.ML"; use "balanced_tree.ML"; use "output.ML"; -use "graph.ML"; use "heap.ML"; use "scan.ML"; use "source.ML"; @@ -25,4 +25,4 @@ use "file.ML"; use "buffer.ML"; use "history.ML"; -use "xml.ML"; +use "markup.ML";