# HG changeset patch
# User wenzelm
# Date 1119127278 -7200
# Node ID eb287ce972308b001f81a796dd1ba5a0193c7f39
# Parent  db2711d07cd8b0fe7a2e536f7e42750ffc8c5d52
added Pure/General/ord_list.ML;

diff -r db2711d07cd8 -r eb287ce97230 src/Pure/General/ROOT.ML
--- 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";
diff -r db2711d07cd8 -r eb287ce97230 src/Pure/IsaMakefile
--- 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		\