diff -r 63fb71d29eba -r 3ec03a3cd9d0 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Feb 25 09:16:16 2010 +0100
+++ b/src/Pure/sign.ML	Thu Feb 25 22:05:34 2010 +0100
@@ -60,6 +60,7 @@
   val intern_term: theory -> term -> term
   val extern_term: theory -> term -> term
   val intern_tycons: theory -> typ -> typ
+  val the_type_decl: theory -> string -> Type.decl
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
   val certify_class: theory -> class -> class
@@ -308,6 +309,7 @@
 
 (* certify wrt. type signature *)
 
+val the_type_decl = Type.the_decl o tsig_of;
 val arity_number = Type.arity_number o tsig_of;
 fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);