tuned sig;
authorwenzelm
Fri, 28 Jan 2000 12:04:17 +0100
changeset 8151 9a2bdaa3c379
parent 8150 7021549ef32d
child 8152 ce3387fafebb
tuned sig;
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