merged
authorberghofe
Tue, 01 Jun 2010 12:16:40 +0200
changeset 37238 d94459cf7ea8
parent 37226 7c59ab0a419b (diff)
parent 37237 957753a47670 (current diff)
child 37239 54b444874be1
child 37245 c1d14288c5c0
merged
--- a/src/Pure/ROOT.ML	Tue Jun 01 11:39:51 2010 +0200
+++ b/src/Pure/ROOT.ML	Tue Jun 01 12:16:40 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*)
+
+