--- 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 *)