src/Pure/ROOT.ML
changeset 42264 b6c1b0c4c511
parent 42243 2f998ff67d0f
child 42284 326f57825e1a
     1.1 --- a/src/Pure/ROOT.ML	Wed Apr 06 22:25:44 2011 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Apr 06 23:04:00 2011 +0200
     1.3 @@ -114,16 +114,16 @@
     1.4  use "sorts.ML";
     1.5  use "type.ML";
     1.6  use "logic.ML";
     1.7 -use "Syntax/lexicon.ML";
     1.8 -use "Syntax/simple_syntax.ML";
     1.9  
    1.10  
    1.11  (* inner syntax *)
    1.12  
    1.13 +use "Syntax/term_position.ML";
    1.14 +use "Syntax/lexicon.ML";
    1.15 +use "Syntax/simple_syntax.ML";
    1.16  use "Syntax/ast.ML";
    1.17  use "Syntax/syn_ext.ML";
    1.18  use "Syntax/parser.ML";
    1.19 -use "Syntax/type_ext.ML";
    1.20  use "Syntax/syn_trans.ML";
    1.21  use "Syntax/mixfix.ML";
    1.22  use "Syntax/printer.ML";