# HG changeset patch
# User wenzelm
# Date 1164402314 -3600
# Node ID 571b8cd087f817f08970515baccd35a864b5978e
# Parent  b165c91207025e6a6c40c26f8d71207bcd4ab6c9
fake predeclaration of structure ProofContext;

diff -r b165c9120702 -r 571b8cd087f8 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;