merged
authorwenzelm
Tue, 01 Jun 2010 11:37:41 +0200
changeset 37226 7c59ab0a419b
parent 37225 32c5251f78cd (current diff)
parent 37220 d416e49b3926 (diff)
child 37238 d94459cf7ea8
merged
--- a/src/Pure/ROOT.ML	Tue Jun 01 11:18:51 2010 +0200
+++ b/src/Pure/ROOT.ML	Tue Jun 01 11:37:41 2010 +0200
@@ -305,9 +305,11 @@
 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;
 
+structure ThyLoad = Thy_Load;  (*Proof General legacy*)
+
+