src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Tue Oct 02 07:59:55 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 02 16:06:41 2007 +0200
@@ -10,6 +10,7 @@
 signature PROOF_CONTEXT =
 sig
   val theory_of: Proof.context -> theory
+  val tsig_of: Proof.context -> Type.tsig
   val init: theory -> Proof.context
   type mode
   val mode_default: mode