# HG changeset patch
# User wenzelm
# Date 1154550411 -7200
# Node ID a9a917b356af4d706c5e52b411852c9d79bcb400
# Parent  753fad9f6e037d5c95b4da7e9e17012b2a7d766e
fake predeclaration of type Proof.context;

diff -r 753fad9f6e03 -r a9a917b356af src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Aug 02 22:26:50 2006 +0200
+++ b/src/Pure/context.ML	Wed Aug 02 22:26:51 2006 +0200
@@ -742,3 +742,6 @@
 
 (*hide private interface*)
 structure Context: CONTEXT = Context;
+
+(*fake predeclaration*)
+structure Proof = struct type context = Context.proof end;