--- 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";
--- a/src/Pure/IsaMakefile Sat Jun 18 22:40:51 2005 +0200
+++ b/src/Pure/IsaMakefile Sat Jun 18 22:41:18 2005 +0200
@@ -26,7 +26,7 @@
$(OUT)/Pure: CPure.thy General/ROOT.ML General/buffer.ML \
General/file.ML General/graph.ML General/heap.ML General/history.ML \
General/lazy_scan.ML General/lazy_seq.ML General/name_space.ML \
- General/object.ML General/output.ML General/path.ML \
+ General/object.ML General/ord_list.ML General/output.ML General/path.ML \
General/position.ML General/pretty.ML General/scan.ML General/seq.ML \
General/source.ML General/susp.ML General/symbol.ML General/table.ML \
General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML \