fake predeclaration of structure ProofContext;
authorwenzelm
Fri Nov 24 22:05:14 2006 +0100 (2006-11-24)
changeset 21518571b8cd087f8
parent 21517 b165c9120702
child 21519 33f109ea389f
fake predeclaration of structure ProofContext;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Fri Nov 24 22:05:13 2006 +0100
     1.2 +++ b/src/Pure/context.ML	Fri Nov 24 22:05:14 2006 +0100
     1.3 @@ -741,5 +741,7 @@
     1.4  (*hide private interface*)
     1.5  structure Context: CONTEXT = Context;
     1.6  
     1.7 -(*fake predeclaration*)
     1.8 +(*fake predeclarations*)
     1.9  structure Proof = struct type context = Context.proof end;
    1.10 +structure ProofContext =
    1.11 +struct val theory_of = Context.theory_of_proof val init = Context.init_proof end;