--- a/src/Pure/General/ROOT.ML Sat Jun 18 22:40:51 2005 +0200
+++ b/src/Pure/General/ROOT.ML Sat Jun 18 22:41:18 2005 +0200
@@ -4,6 +4,7 @@
Library of general tools --- prefer this over the 'Standard ML Library'.
*)
+use "ord_list.ML";
use "table.ML";
use "output.ML";
use "graph.ML";