# HG changeset patch
# User wenzelm
# Date 1085835625 -7200
# Node ID ebb8499d0fd2c86577e6db7a0dfe1b8535e99fba
# Parent  c5fcde6324a2867d1262b0846ac86bd92e8bd300
moved print_mode to General/output.ML; load General/pretty.ML early;

diff -r c5fcde6324a2 -r ebb8499d0fd2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat May 29 15:00:14 2004 +0200
+++ b/src/Pure/ROOT.ML	Sat May 29 15:00:25 2004 +0200
@@ -12,9 +12,6 @@
 
 print_depth 10;
 
-(*global flags*)
-val print_mode = ref ([]: string list);
-
 (*fake hiding of private structures*)
 structure Hidden = struct end;
 
@@ -24,6 +21,7 @@
 
 (*fundamental structures*)
 use "term.ML";
+use "General/pretty.ML";
 use "sorts.ML";
 use "type.ML";