# HG changeset patch
# User wenzelm
# Date 949057457 -3600
# Node ID 9a2bdaa3c379b975b4c023dc7bf9212c96c9d443
# Parent  7021549ef32d983aba28270042adc87ea4dc34a1
tuned sig;

diff -r 7021549ef32d -r 9a2bdaa3c379 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Jan 28 12:03:59 2000 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Jan 28 12:04:17 2000 +0100
@@ -73,7 +73,7 @@
   val setup: (theory -> theory) list
 end;
 
-signature PROOF_CONTEXT_PRIVATE =
+signature PRIVATE_PROOF_CONTEXT =
 sig
   include PROOF_CONTEXT
   val init_data: Object.kind -> (theory -> Object.T) * (context -> Object.T -> unit)
@@ -83,7 +83,7 @@
   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> context -> context
 end;
 
-structure ProofContext: PROOF_CONTEXT_PRIVATE =
+structure ProofContext: PRIVATE_PROOF_CONTEXT =
 struct