src/HOL/HOL.ML

--- a/src/HOL/HOL.ML	Fri Feb 03 08:48:16 2006 +0100
+++ b/src/HOL/HOL.ML	Fri Feb 03 08:48:33 2006 +0100
@@ -4,7 +4,6 @@
 
 structure HOL =
 struct
-  val thy = the_context ();
   val eq_reflection = eq_reflection;
   val refl = refl;
   val subst = subst;
@@ -26,3 +25,12 @@
 end;
 
 open HOL;
+
+structure HOL =
+struct
+
+open HOL;
+
+val thy = the_context ();
+
+end;