--- a/src/HOL/HOL.ML Fri Jul 21 10:28:32 2000 +0200 +++ b/src/HOL/HOL.ML Fri Jul 21 12:30:08 2000 +0200 @@ -1,4 +1,3 @@ - structure HOL = struct val thy = the_context ();