--- a/src/Pure/context.ML Sun Jan 21 16:43:47 2007 +0100 +++ b/src/Pure/context.ML Sun Jan 21 16:46:06 2007 +0100 @@ -681,7 +681,6 @@ end; - (*hide private interface*) structure Context: CONTEXT = Context;