# HG changeset patch # User wenzelm # Date 1188293130 -7200 # Node ID cad0644294a9250a385cc83c3bf729543f7b69d3 # Parent 448978b61556422ace84c36e724f6cc33053a6af tuned load order -- minimizes modules before Secure; diff -r 448978b61556 -r cad0644294a9 src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Tue Aug 28 11:25:29 2007 +0200 +++ b/src/Pure/General/ROOT.ML Tue Aug 28 11:25:30 2007 +0200 @@ -5,19 +5,20 @@ *) use "print_mode.ML"; -use "stack.ML"; -use "ord_list.ML"; use "alist.ML"; use "table.ML"; -use "graph.ML"; -use "balanced_tree.ML"; use "output.ML"; use "markup.ML"; -use "heap.ML"; use "scan.ML"; use "source.ML"; use "symbol.ML"; use "secure.ML"; + +use "stack.ML"; +use "heap.ML"; +use "ord_list.ML"; +use "balanced_tree.ML"; +use "graph.ML"; use "name_space.ML"; use "seq.ML"; use "susp.ML";