do not open ML structures;

--- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 16:29:13 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 16:37:21 2011 +0200
@@ -164,7 +164,9 @@
 structure Proof_Context: PROOF_CONTEXT =
 struct
 
-open Proof_Context;
+val theory_of = Proof_Context.theory_of;
+val init_global = Proof_Context.init_global;
+
 
 
 (** inner syntax mode **)