1.1 --- a/src/Pure/General/ROOT.ML	Fri Jun 05 08:00:53 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,40 +0,0 @@
     1.4 -(*  Title:      Pure/General/ROOT.ML
     1.5 -
     1.6 -Library of general tools.
     1.7 -*)
     1.8 -
     1.9 -use "print_mode.ML";
    1.10 -use "alist.ML";
    1.11 -use "table.ML";
    1.12 -use "output.ML";
    1.13 -use "properties.ML";
    1.14 -use "markup.ML";
    1.15 -use "scan.ML";
    1.16 -use "source.ML";
    1.17 -use "symbol.ML";
    1.18 -use "seq.ML";
    1.19 -use "position.ML";
    1.20 -use "symbol_pos.ML";
    1.21 -use "antiquote.ML";
    1.22 -use "../ML/ml_lex.ML";
    1.23 -use "../ML/ml_parse.ML";
    1.24 -use "secure.ML";
    1.25 -
    1.26 -use "integer.ML";
    1.27 -use "stack.ML";
    1.28 -use "queue.ML";
    1.29 -use "heap.ML";
    1.30 -use "ord_list.ML";
    1.31 -use "balanced_tree.ML";
    1.32 -use "graph.ML";
    1.33 -use "long_name.ML";
    1.34 -use "binding.ML";
    1.35 -use "name_space.ML";
    1.36 -use "lazy.ML";
    1.37 -use "path.ML";
    1.38 -use "url.ML";
    1.39 -use "buffer.ML";
    1.40 -use "file.ML";
    1.41 -use "xml.ML";
    1.42 -use "yxml.ML";
    1.43 -