diff -r d3bc9c1ff241 -r 26d5f3bcc933 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Apr 25 22:23:04 2006 +0200
+++ b/src/Pure/sign.ML	Tue Apr 25 22:23:11 2006 +0200
@@ -152,6 +152,8 @@
   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
@@ -412,6 +414,9 @@
 
 (* 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;
@@ -561,11 +566,8 @@
 (* 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;