src/Pure/sign.ML
changeset 35359 3ec03a3cd9d0
parent 35262 9ea4445d2ccf
child 35395 ba804f4c82c6
     1.1 --- a/src/Pure/sign.ML	Thu Feb 25 09:16:16 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Feb 25 22:05:34 2010 +0100
     1.3 @@ -60,6 +60,7 @@
     1.4    val intern_term: theory -> term -> term
     1.5    val extern_term: theory -> term -> term
     1.6    val intern_tycons: theory -> typ -> typ
     1.7 +  val the_type_decl: theory -> string -> Type.decl
     1.8    val arity_number: theory -> string -> int
     1.9    val arity_sorts: theory -> string -> sort -> sort list
    1.10    val certify_class: theory -> class -> class
    1.11 @@ -308,6 +309,7 @@
    1.12  
    1.13  (* certify wrt. type signature *)
    1.14  
    1.15 +val the_type_decl = Type.the_decl o tsig_of;
    1.16  val arity_number = Type.arity_number o tsig_of;
    1.17  fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
    1.18