author | haftmann |
Fri, 03 Feb 2006 08:48:33 +0100 | |
changeset 18916 | fda5b8dbbef6 |
parent 18915 | 7521b849ae98 |
child 18917 | 77e18862990f |
src/HOL/HOL.ML | file | annotate | diff | comparison | revisions |
--- 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;