src/Pure/sign.ML

   val string_of_classrel: theory -> class list -> string
   val string_of_arity: theory -> arity -> string
   val pprint_term: theory -> term -> pprint_args -> unit
   val pprint_typ: theory -> typ -> pprint_args -> unit
   val pp: theory -> Pretty.pp
+  val arity_number: theory -> string -> int
+  val arity_sorts: theory -> string -> sort -> sort list
   val certify_class: theory -> class -> class
   val certify_sort: theory -> sort -> sort
   val certify_typ: theory -> typ -> typ
   val certify_typ_syntax: theory -> typ -> typ
   val certify_typ_abbrev: theory -> typ -> typ

 
 (** certify entities **)    (*exception TYPE*)
 
 (* certify wrt. type signature *)
 
+val arity_number = Type.arity_number o tsig_of;
+fun arity_sorts thy = Type.arity_sorts (pp thy) (tsig_of thy);
+
 fun certify cert = cert o tsig_of o Context.check_thy;
 
 val certify_class      = certify Type.cert_class;
 val certify_sort       = certify Type.cert_sort;
 val certify_typ        = certify Type.cert_typ;

 
 
 (* type and constant names *)
 
 fun read_tyname thy raw_c =
-  let val c = intern_type thy raw_c in
-    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
-      SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
-    | _ => error ("Undeclared type constructor: " ^ quote c))
-  end;
+  let val c = intern_type thy raw_c
+  in Type (c, replicate (arity_number thy c) dummyT) end;
 
 val read_const = Consts.read_const o consts_of;