# HG changeset patch
# User wenzelm
# Date 1274084455 -7200
# Node ID 226fb165833ec8cea59fcc90f734d0b57c58b61c
# Parent  ef698bd61057c3ee67607b32ae8267fcc53ae1b6
centralized legacy aliases;

diff -r ef698bd61057 -r 226fb165833e src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Sun May 16 00:02:11 2010 +0200
+++ b/src/Pure/Isar/keyword.ML	Mon May 17 10:20:55 2010 +0200
@@ -210,7 +210,4 @@
 
 end;
 
-(*legacy alias*)
-structure OuterKeyword = Keyword;
 
-
diff -r ef698bd61057 -r 226fb165833e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sun May 16 00:02:11 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon May 17 10:20:55 2010 +0200
@@ -297,6 +297,3 @@
 
 end;
 
-(*legacy alias*)
-structure OuterSyntax = Outer_Syntax;
-
diff -r ef698bd61057 -r 226fb165833e src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun May 16 00:02:11 2010 +0200
+++ b/src/Pure/Isar/parse.ML	Mon May 17 10:20:55 2010 +0200
@@ -341,6 +341,3 @@
 type 'a parser = 'a Parse.parser;
 type 'a context_parser = 'a Parse.context_parser;
 
-(*legacy alias*)
-structure OuterParse = Parse;
-
diff -r ef698bd61057 -r 226fb165833e src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Sun May 16 00:02:11 2010 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Mon May 17 10:20:55 2010 +0200
@@ -162,6 +162,3 @@
 
 end;
 
-(*legacy alias*)
-structure SpecParse = Parse_Spec;
-
diff -r ef698bd61057 -r 226fb165833e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun May 16 00:02:11 2010 +0200
+++ b/src/Pure/ROOT.ML	Mon May 17 10:20:55 2010 +0200
@@ -292,3 +292,17 @@
 
 use "pure_setup.ML";
 
+
+(* legacy aliases *)
+
+structure Legacy =
+struct
+
+structure OuterKeyword = Keyword;
+structure OuterParse = Parse;
+structure OuterSyntax = Outer_Syntax;
+structure SpecParse = Parse_Spec;
+
+end;
+
+open Legacy;  (* FIXME *)