src/Pure/ROOT.ML
changeset 36959 f5417836dbea
parent 36955 226fb165833e
child 36961 7b14afc02fc4
     1.1 --- a/src/Pure/ROOT.ML	Mon May 17 15:05:32 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon May 17 15:11:25 2010 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4  use "Proof/proofchecker.ML";
     1.5  
     1.6  (*outer syntax*)
     1.7 -use "Isar/outer_lex.ML";
     1.8 +use "Isar/token.ML";
     1.9  use "Isar/keyword.ML";
    1.10  use "Isar/parse.ML";
    1.11  use "Isar/parse_value.ML";
    1.12 @@ -299,6 +299,13 @@
    1.13  struct
    1.14  
    1.15  structure OuterKeyword = Keyword;
    1.16 +
    1.17 +structure OuterLex =
    1.18 +struct
    1.19 +  open Token;
    1.20 +  type token = T;
    1.21 +end;
    1.22 +
    1.23  structure OuterParse = Parse;
    1.24  structure OuterSyntax = Outer_Syntax;
    1.25  structure SpecParse = Parse_Spec;