src/Pure/ROOT.ML
changeset 37220 d416e49b3926
parent 37216 3165bc303f66
child 37239 54b444874be1
     1.1 --- a/src/Pure/ROOT.ML	Tue Jun 01 09:12:12 2010 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Jun 01 11:37:24 2010 +0200
     1.3 @@ -305,9 +305,11 @@
     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 +