load type_infer.ML after Syntax module;
authorwenzelm
Wed, 18 Jun 2008 22:32:01 +0200
changeset 27262 5a5d7f55ec19
parent 27261 5b3101338f42
child 27263 a6b7f934fbc4
load type_infer.ML after Syntax module;
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*)