no toplevel 'thy' anymore
authorhaftmann
Fri, 03 Feb 2006 08:48:33 +0100
changeset 18916 fda5b8dbbef6
parent 18915 7521b849ae98
child 18917 77e18862990f
no toplevel 'thy' anymore
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;