# HG changeset patch
# User wenzelm
# Date 1191334001 -7200
# Node ID 8c2e8cf22fad4f477940ca1c9a338de7b36acdbb
# Parent  3bf788a0c49ab480b992a51b9784e5cc35305b37
export tsig_of;

diff -r 3bf788a0c49a -r 8c2e8cf22fad 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