# HG changeset patch
# User wenzelm
# Date 1165860320 -3600
# Node ID b82f344f7922871ea4cc8dc96d50a89bcbf8d383
# Parent  69165d27b55b8be1346d6390bfe570d7ea00180b
load secure.ML after symbol.ML, when default output is active;

diff -r 69165d27b55b -r b82f344f7922 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";