src/Pure/context.ML

--- a/src/Pure/context.ML	Fri Nov 24 22:05:13 2006 +0100
+++ b/src/Pure/context.ML	Fri Nov 24 22:05:14 2006 +0100
@@ -741,5 +741,7 @@
 (*hide private interface*)
 structure Context: CONTEXT = Context;
 
-(*fake predeclaration*)
+(*fake predeclarations*)
 structure Proof = struct type context = Context.proof end;
+structure ProofContext =
+struct val theory_of = Context.theory_of_proof val init = Context.init_proof end;