# HG changeset patch
# User wenzelm
# Date 1275385061 -7200
# Node ID 7c59ab0a419b20c5597e1daf930a3a1c94c91d24
# Parent  32c5251f78cdd5a2c42ae9dac9309d2032f5cdcb# Parent  d416e49b3926a13c5a4b09e5802a74e605bbdf7a
merged

diff -r 32c5251f78cd -r 7c59ab0a419b src/Pure/ROOT.ML
--- 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*)
+
+