# HG changeset patch
# User wenzelm
# Date 1302964641 -7200
# Node ID e52e3f697510a9f105d654065b63078269d9c0a2
# Parent  5528970ac6f7d0e17e3bc6410b919e46c647b342
do not open ML structures;

diff -r 5528970ac6f7 -r e52e3f697510 src/Pure/Isar/proof_context.ML
--- 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 **)