# HG changeset patch
# User haftmann
# Date 1138952913 -3600
# Node ID fda5b8dbbef6b4bbe65a0d8e331b2fd1efb0ce7b
# Parent  7521b849ae980a16b6668beeafd25274b68bf88b
no toplevel 'thy' anymore

diff -r 7521b849ae98 -r fda5b8dbbef6 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;