--- 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);