centralized legacy aliases;
authorwenzelm
Mon, 17 May 2010 10:20:55 +0200
changeset 36955 226fb165833e
parent 36954 ef698bd61057
child 36956 21be4832c362
centralized legacy aliases;
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse_spec.ML
src/Pure/ROOT.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;
 
-
--- 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;
-
--- 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;
-
--- 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;
-
--- 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 *)