src/Pure/ROOT.ML
changeset 36955 226fb165833e
parent 36952 338c3f8229e4
child 36959 f5417836dbea
     1.1 --- a/src/Pure/ROOT.ML	Sun May 16 00:02:11 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon May 17 10:20:55 2010 +0200
     1.3 @@ -292,3 +292,17 @@
     1.4  
     1.5  use "pure_setup.ML";
     1.6  
     1.7 +
     1.8 +(* legacy aliases *)
     1.9 +
    1.10 +structure Legacy =
    1.11 +struct
    1.12 +
    1.13 +structure OuterKeyword = Keyword;
    1.14 +structure OuterParse = Parse;
    1.15 +structure OuterSyntax = Outer_Syntax;
    1.16 +structure SpecParse = Parse_Spec;
    1.17 +
    1.18 +end;
    1.19 +
    1.20 +open Legacy;  (* FIXME *)