# HG changeset patch
# User wenzelm
# Date 1187126573 -7200
# Node ID 2f85bae2e2c2a4b73a58a0bf202b8c4bf8c1f509
# Parent  49960810117720cefeb9046114372a8621336887
tuned order;

diff -r 499608101177 -r 2f85bae2e2c2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Aug 14 23:22:51 2007 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 14 23:22:53 2007 +0200
@@ -26,13 +26,13 @@
 use "General/pretty.ML";
 use "Syntax/lexicon.ML";
 use "Syntax/simple_syntax.ML";
-use "sorts.ML";
-use "type.ML";
 use "context.ML";
 use "context_position.ML";
+use "sorts.ML";
+use "type.ML";
+use "type_infer.ML";
 use "config.ML";
 use "compress.ML";
-use "type_infer.ML";
 
 (*inner syntax module*)
 use "Syntax/ast.ML";