changeset 21769 | b82f344f7922 |
parent 21157 | dae0416fddfd |
child 22952 | 5b7259f3654e |
--- a/src/Pure/General/ROOT.ML Mon Dec 11 16:58:19 2006 +0100 +++ b/src/Pure/General/ROOT.ML Mon Dec 11 19:05:20 2006 +0100 @@ -9,12 +9,12 @@ use "alist.ML"; use "table.ML"; use "output.ML"; -use "secure.ML"; use "graph.ML"; use "heap.ML"; use "scan.ML"; use "source.ML"; use "symbol.ML"; +use "secure.ML"; use "name_space.ML"; use "seq.ML"; use "susp.ML";