src/Pure/ROOT.ML
changeset 22694 077ce0e019fa
parent 22679 68cd69a388e2
child 22796 34c316d7b630
     1.1 --- a/src/Pure/ROOT.ML	Sun Apr 15 14:31:51 2007 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Sun Apr 15 14:31:52 2007 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4  use "type.ML";
     1.5  use "context.ML";
     1.6  use "compress.ML";
     1.7 +use "type_infer.ML";
     1.8  
     1.9  (*inner syntax module*)
    1.10  use "Syntax/lexicon.ML";
    1.11 @@ -50,7 +51,6 @@
    1.12  structure Mixfix = Hidden;
    1.13  structure Printer = Hidden;
    1.14  
    1.15 -use "type_infer.ML";
    1.16  use "General/ml_syntax.ML";
    1.17  
    1.18  (*core of tactical proof system*)