# HG changeset patch
# User wenzelm
# Date 1185652858 -7200
# Node ID a1afcff544a64c81f9a5567082541ac7f4bfef9a
# Parent  8a4d5312d378b684c4e7b63c4a33e78b65496cdb
use config_option.ML after sign.ML;

diff -r 8a4d5312d378 -r a1afcff544a6 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Jul 28 21:09:14 2007 +0200
+++ b/src/Pure/ROOT.ML	Sat Jul 28 22:00:58 2007 +0200
@@ -41,7 +41,6 @@
 use "Syntax/printer.ML";
 use "Syntax/syntax.ML";
 
-use "config_option.ML";
 use "General/ml_syntax.ML";
 
 (*core of tactical proof system*)
@@ -49,6 +48,7 @@
 use "logic.ML";
 use "consts.ML";
 use "sign.ML";
+use "config_option.ML";
 use "pattern.ML";
 use "unify.ML";
 use "net.ML";