src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Thu Jul 16 00:24:11 2009 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 16 16:24:49 2009 +0200
@@ -33,11 +33,12 @@
 use "ML/ml_lex.ML";
 use "ML/ml_parse.ML";
 use "General/secure.ML";
-(*----- basic ML bootstrap finished -----*)
+(*^^^^^ end of basic ML bootstrap ^^^^^*)
 use "General/integer.ML";
 use "General/stack.ML";
 use "General/queue.ML";
 use "General/heap.ML";
+use "General/same.ML";
 use "General/ord_list.ML";
 use "General/balanced_tree.ML";
 use "General/graph.ML";