# HG changeset patch
# User wenzelm
# Date 1213821121 -7200
# Node ID 5a5d7f55ec1956323a8eed21c25a99ad4b93a89b
# Parent  5b3101338f421ab61613b35d3ea8b297741d7305
load type_infer.ML after Syntax module;

diff -r 5b3101338f42 -r 5a5d7f55ec19 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Jun 18 18:55:10 2008 +0200
+++ b/src/Pure/ROOT.ML	Wed Jun 18 22:32:01 2008 +0200
@@ -32,7 +32,6 @@
 use "context.ML";
 use "sorts.ML";
 use "type.ML";
-use "type_infer.ML";
 use "config.ML";
 
 (*inner syntax module*)
@@ -45,6 +44,7 @@
 use "Syntax/printer.ML";
 use "Syntax/syntax.ML";
 
+use "type_infer.ML";
 use "ML/ml_syntax.ML";
 
 (*core of tactical proof system*)