changeset 23613 | 3f2a6c66e089 |
parent 23420 | 6f60a90e52e5 |
child 23625 | 2d32185530d7 |
--- 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";