src/Pure/ROOT.ML
changeset 37244 54b444874be1
parent 37225 d416e49b3926
child 37782 71dd62132eda
     1.1 --- a/src/Pure/ROOT.ML	Tue Jun 01 12:16:40 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Jun 01 13:32:05 2010 +0200
     1.3 @@ -305,11 +305,9 @@
     1.4  structure PrintMode = Print_Mode;
     1.5  structure SpecParse = Parse_Spec;
     1.6  structure ThyInfo = Thy_Info;
     1.7 +structure ThyLoad = Thy_Load;
     1.8  structure ThyOutput = Thy_Output;
     1.9  structure TypeInfer = Type_Infer;
    1.10  
    1.11  end;
    1.12  
    1.13 -structure ThyLoad = Thy_Load;  (*Proof General legacy*)
    1.14 -
    1.15 -