src/Pure/sign.ML
changeset 19462 26d5f3bcc933
parent 19427 f086002893ad
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/sign.ML	Tue Apr 25 22:23:04 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Apr 25 22:23:11 2006 +0200
     1.3 @@ -152,6 +152,8 @@
     1.4    val pprint_term: theory -> term -> pprint_args -> unit
     1.5    val pprint_typ: theory -> typ -> pprint_args -> unit
     1.6    val pp: theory -> Pretty.pp
     1.7 +  val arity_number: theory -> string -> int
     1.8 +  val arity_sorts: theory -> string -> sort -> sort list
     1.9    val certify_class: theory -> class -> class
    1.10    val certify_sort: theory -> sort -> sort
    1.11    val certify_typ: theory -> typ -> typ
    1.12 @@ -412,6 +414,9 @@
    1.13  
    1.14  (* certify wrt. type signature *)
    1.15  
    1.16 +val arity_number = Type.arity_number o tsig_of;
    1.17 +fun arity_sorts thy = Type.arity_sorts (pp thy) (tsig_of thy);
    1.18 +
    1.19  fun certify cert = cert o tsig_of o Context.check_thy;
    1.20  
    1.21  val certify_class      = certify Type.cert_class;
    1.22 @@ -561,11 +566,8 @@
    1.23  (* type and constant names *)
    1.24  
    1.25  fun read_tyname thy raw_c =
    1.26 -  let val c = intern_type thy raw_c in
    1.27 -    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
    1.28 -      SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
    1.29 -    | _ => error ("Undeclared type constructor: " ^ quote c))
    1.30 -  end;
    1.31 +  let val c = intern_type thy raw_c
    1.32 +  in Type (c, replicate (arity_number thy c) dummyT) end;
    1.33  
    1.34  val read_const = Consts.read_const o consts_of;
    1.35