added is_type_abbr;
authorwenzelm
Fri Apr 14 17:29:57 2000 +0200 (2000-04-14)
changeset 87152cdabe1bb350
parent 8714 61cafd91963c
child 8716 49ac76cf0d54
added is_type_abbr;
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/sign.ML	Fri Apr 14 16:12:46 2000 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Apr 14 17:29:57 2000 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4    val of_sort: sg -> typ * sort -> bool
     1.5    val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
     1.6    val univ_witness: sg -> (typ * sort) option
     1.7 +  val is_type_abbr: sg -> string -> bool
     1.8    val classK: string
     1.9    val typeK: string
    1.10    val constK: string
    1.11 @@ -267,6 +268,7 @@
    1.12  val of_sort = Type.of_sort o tsig_of;
    1.13  val witness_sorts = Type.witness_sorts o tsig_of;
    1.14  val univ_witness = Type.univ_witness o tsig_of;
    1.15 +val is_type_abbr = Type.is_type_abbr o tsig_of;
    1.16  
    1.17  
    1.18  
     2.1 --- a/src/Pure/type.ML	Fri Apr 14 16:12:46 2000 +0200
     2.2 +++ b/src/Pure/type.ML	Fri Apr 14 17:29:57 2000 +0200
     2.3 @@ -29,6 +29,7 @@
     2.4    val defaultS: type_sig -> sort
     2.5    val logical_types: type_sig -> string list
     2.6    val univ_witness: type_sig -> (typ * sort) option
     2.7 +  val is_type_abbr: type_sig -> string -> bool
     2.8    val subsort: type_sig -> sort * sort -> bool
     2.9    val eq_sort: type_sig -> sort * sort -> bool
    2.10    val norm_sort: type_sig -> sort -> sort
    2.11 @@ -178,6 +179,7 @@
    2.12  fun defaultS (TySg {default, ...}) = default;
    2.13  fun logical_types (TySg {log_types, ...}) = log_types;
    2.14  fun univ_witness (TySg {univ_witness, ...}) = univ_witness;
    2.15 +fun is_type_abbr (TySg {abbrs, ...}) name = is_some (Symtab.lookup (abbrs, name));
    2.16  
    2.17  
    2.18  (* sorts *)