load type_infer.ML after Syntax module;
authorwenzelm
Wed Jun 18 22:32:01 2008 +0200 (2008-06-18)
changeset 272625a5d7f55ec19
parent 27261 5b3101338f42
child 27263 a6b7f934fbc4
load type_infer.ML after Syntax module;
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Wed Jun 18 18:55:10 2008 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Jun 18 22:32:01 2008 +0200
     1.3 @@ -32,7 +32,6 @@
     1.4  use "context.ML";
     1.5  use "sorts.ML";
     1.6  use "type.ML";
     1.7 -use "type_infer.ML";
     1.8  use "config.ML";
     1.9  
    1.10  (*inner syntax module*)
    1.11 @@ -45,6 +44,7 @@
    1.12  use "Syntax/printer.ML";
    1.13  use "Syntax/syntax.ML";
    1.14  
    1.15 +use "type_infer.ML";
    1.16  use "ML/ml_syntax.ML";
    1.17  
    1.18  (*core of tactical proof system*)