# HG changeset patch
# User wenzelm
# Date 1120221719 -7200
# Node ID 3e4d726aaed1a1067716c15b2d8e8b377607fe6b
# Parent  d964cbaa6c1cd669f7b4fdff74db2457b4934051
added all_sorts_nonempty;

diff -r d964cbaa6c1c -r 3e4d726aaed1 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Jul 01 14:41:58 2005 +0200
+++ b/src/Pure/sign.ML	Fri Jul 01 14:41:59 2005 +0200
@@ -90,6 +90,7 @@
   val of_sort: theory -> typ * sort -> bool
   val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
   val universal_witness: theory -> (typ * sort) option
+  val all_sorts_nonempty: theory -> bool
   val typ_instance: theory -> typ * typ -> bool
   val is_logtype: theory -> string -> bool
   val const_type: theory -> string -> typ option
@@ -246,6 +247,7 @@
 val of_sort = Type.of_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
 val universal_witness = Type.universal_witness o tsig_of;
+val all_sorts_nonempty = is_some o universal_witness;
 val typ_instance = Type.typ_instance o tsig_of;
 fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);