1.1 --- a/src/Pure/ROOT.ML	Thu Jul 16 00:24:11 2009 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Thu Jul 16 16:24:49 2009 +0200
     1.3 @@ -33,11 +33,12 @@
     1.4  use "ML/ml_lex.ML";
     1.5  use "ML/ml_parse.ML";
     1.6  use "General/secure.ML";
     1.7 -(*----- basic ML bootstrap finished -----*)
     1.8 +(*^^^^^ end of basic ML bootstrap ^^^^^*)
     1.9  use "General/integer.ML";
    1.10  use "General/stack.ML";
    1.11  use "General/queue.ML";
    1.12  use "General/heap.ML";
    1.13 +use "General/same.ML";
    1.14  use "General/ord_list.ML";
    1.15  use "General/balanced_tree.ML";
    1.16  use "General/graph.ML";