removed legacy aliases;
authorwenzelm
Mon Jul 12 22:07:36 2010 +0200 (2010-07-12)
changeset 3778271dd62132eda
parent 37781 2fbbf0a48cef
child 37783 95aa0afcb240
removed legacy aliases;
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Mon Jul 12 21:38:37 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Jul 12 22:07:36 2010 +0200
     1.3 @@ -292,22 +292,3 @@
     1.4  
     1.5  use "pure_setup.ML";
     1.6  
     1.7 -
     1.8 -(* legacy aliases *)
     1.9 -
    1.10 -structure Legacy =
    1.11 -struct
    1.12 -
    1.13 -structure OuterKeyword = Keyword;
    1.14 -structure OuterLex = struct open Token type token = T end;
    1.15 -structure OuterParse = Parse;
    1.16 -structure OuterSyntax = Outer_Syntax;
    1.17 -structure PrintMode = Print_Mode;
    1.18 -structure SpecParse = Parse_Spec;
    1.19 -structure ThyInfo = Thy_Info;
    1.20 -structure ThyLoad = Thy_Load;
    1.21 -structure ThyOutput = Thy_Output;
    1.22 -structure TypeInfer = Type_Infer;
    1.23 -
    1.24 -end;
    1.25 -