1.1 --- a/src/Pure/Isar/keyword.ML	Sun May 16 00:02:11 2010 +0200
     1.2 +++ b/src/Pure/Isar/keyword.ML	Mon May 17 10:20:55 2010 +0200
     1.3 @@ -210,7 +210,4 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -(*legacy alias*)
     1.8 -structure OuterKeyword = Keyword;
     1.9  
    1.10 -

     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun May 16 00:02:11 2010 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon May 17 10:20:55 2010 +0200
     2.3 @@ -297,6 +297,3 @@
     2.4  
     2.5  end;
     2.6  
     2.7 -(*legacy alias*)
     2.8 -structure OuterSyntax = Outer_Syntax;
     2.9 -

     3.1 --- a/src/Pure/Isar/parse.ML	Sun May 16 00:02:11 2010 +0200
     3.2 +++ b/src/Pure/Isar/parse.ML	Mon May 17 10:20:55 2010 +0200
     3.3 @@ -341,6 +341,3 @@
     3.4  type 'a parser = 'a Parse.parser;
     3.5  type 'a context_parser = 'a Parse.context_parser;
     3.6  
     3.7 -(*legacy alias*)
     3.8 -structure OuterParse = Parse;
     3.9 -

     4.1 --- a/src/Pure/Isar/parse_spec.ML	Sun May 16 00:02:11 2010 +0200
     4.2 +++ b/src/Pure/Isar/parse_spec.ML	Mon May 17 10:20:55 2010 +0200
     4.3 @@ -162,6 +162,3 @@
     4.4  
     4.5  end;
     4.6  
     4.7 -(*legacy alias*)
     4.8 -structure SpecParse = Parse_Spec;
     4.9 -

     5.1 --- a/src/Pure/ROOT.ML	Sun May 16 00:02:11 2010 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Mon May 17 10:20:55 2010 +0200
     5.3 @@ -292,3 +292,17 @@
     5.4  
     5.5  use "pure_setup.ML";
     5.6  
     5.7 +
     5.8 +(* legacy aliases *)
     5.9 +
    5.10 +structure Legacy =
    5.11 +struct
    5.12 +
    5.13 +structure OuterKeyword = Keyword;
    5.14 +structure OuterParse = Parse;
    5.15 +structure OuterSyntax = Outer_Syntax;
    5.16 +structure SpecParse = Parse_Spec;
    5.17 +
    5.18 +end;
    5.19 +
    5.20 +open Legacy;  (* FIXME *)