fake predeclaration of structure ProofContext;
authorwenzelm
Fri, 24 Nov 2006 22:05:14 +0100
changeset 21518 571b8cd087f8
parent 21517 b165c9120702
child 21519 33f109ea389f
fake predeclaration of structure ProofContext;
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;