author | wenzelm |
Fri, 24 Nov 2006 22:05:14 +0100 | |
changeset 21518 | 571b8cd087f8 |
parent 21517 | b165c9120702 |
child 21519 | 33f109ea389f |
--- 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;