load secure.ML after symbol.ML, when default output is active;
authorwenzelm
Mon, 11 Dec 2006 19:05:20 +0100
changeset 21769 b82f344f7922
parent 21768 69165d27b55b
child 21770 ea6f846d8c4b
load secure.ML after symbol.ML, when default output is active;
src/Pure/General/ROOT.ML
--- 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";