# HG changeset patch
# User wenzelm
# Date 1269464883 -3600
# Node ID a6f36926280461d90f1db2f3d4ec4775ef34ab5e
# Parent  ed52ade112c00b56ada64b8bc93339a1ff4e5d1f# Parent  65d8cfff417f00d6ed81b3133a77788c2a169377
merged

diff -r ed52ade112c0 -r a6f369262804 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Mar 24 17:41:25 2010 +0100
+++ b/src/Pure/ROOT.ML	Wed Mar 24 22:08:03 2010 +0100
@@ -92,14 +92,14 @@
 use "term_ord.ML";
 use "term_subst.ML";
 use "old_term.ML";
-use "logic.ML";
 use "General/pretty.ML";
 use "context.ML";
 use "context_position.ML";
+use "sorts.ML";
+use "type.ML";
+use "logic.ML";
 use "Syntax/lexicon.ML";
 use "Syntax/simple_syntax.ML";
-use "sorts.ML";
-use "type.ML";
 use "config.ML";