# HG changeset patch
# User wenzelm
# Date 1278965256 -7200
# Node ID 71dd62132eda2a89f7e1624edfe28afe23c98332
# Parent  2fbbf0a48cef5600244a607f7fe636efbe5d565f
removed legacy aliases;

diff -r 2fbbf0a48cef -r 71dd62132eda src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jul 12 21:38:37 2010 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 12 22:07:36 2010 +0200
@@ -292,22 +292,3 @@
 
 use "pure_setup.ML";
 
-
-(* legacy aliases *)
-
-structure Legacy =
-struct
-
-structure OuterKeyword = Keyword;
-structure OuterLex = struct open Token type token = T end;
-structure OuterParse = Parse;
-structure OuterSyntax = Outer_Syntax;
-structure PrintMode = Print_Mode;
-structure SpecParse = Parse_Spec;
-structure ThyInfo = Thy_Info;
-structure ThyLoad = Thy_Load;
-structure ThyOutput = Thy_Output;
-structure TypeInfer = Type_Infer;
-
-end;
-