src/Pure/ROOT.ML
changeset 26629 6e93fbd4c96a
parent 26279 e8440c90c474
child 27254 0f8106808e66
equal deleted inserted replaced
26628:63306cb94313 26629:6e93fbd4c96a
    32 use "context.ML";
    32 use "context.ML";
    33 use "sorts.ML";
    33 use "sorts.ML";
    34 use "type.ML";
    34 use "type.ML";
    35 use "type_infer.ML";
    35 use "type_infer.ML";
    36 use "config.ML";
    36 use "config.ML";
    37 use "compress.ML";
       
    38 
    37 
    39 (*inner syntax module*)
    38 (*inner syntax module*)
    40 use "Syntax/ast.ML";
    39 use "Syntax/ast.ML";
    41 use "Syntax/syn_ext.ML";
    40 use "Syntax/syn_ext.ML";
    42 use "Syntax/parser.ML";
    41 use "Syntax/parser.ML";