export tsig_of;
authorwenzelm
Tue, 02 Oct 2007 16:06:41 +0200
changeset 24812 8c2e8cf22fad
parent 24811 3bf788a0c49a
child 24813 74bc59c2c4a6
export tsig_of;
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