src/Pure/sign.ML
changeset 16655 3e4d726aaed1
parent 16597 5a5229a55964
child 16723 9a9c034f1d57
     1.1 --- a/src/Pure/sign.ML	Fri Jul 01 14:41:58 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Jul 01 14:41:59 2005 +0200
     1.3 @@ -90,6 +90,7 @@
     1.4    val of_sort: theory -> typ * sort -> bool
     1.5    val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
     1.6    val universal_witness: theory -> (typ * sort) option
     1.7 +  val all_sorts_nonempty: theory -> bool
     1.8    val typ_instance: theory -> typ * typ -> bool
     1.9    val is_logtype: theory -> string -> bool
    1.10    val const_type: theory -> string -> typ option
    1.11 @@ -246,6 +247,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 universal_witness = Type.universal_witness o tsig_of;
    1.15 +val all_sorts_nonempty = is_some o universal_witness;
    1.16  val typ_instance = Type.typ_instance o tsig_of;
    1.17  fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
    1.18