Added nonempty_sort.

--- a/src/Pure/sign.ML	Fri Jul 28 19:17:03 1995 +0200
+++ b/src/Pure/sign.ML	Tue Aug 01 12:36:05 1995 +0200
@@ -62,6 +62,7 @@
     val add_name: string -> sg -> sg
     val make_draft: sg -> sg
     val merge: sg * sg -> sg
+    val nonempty_sort: sg * sort list * sort -> bool
     val proto_pure: sg
     val pure: sg
     val cpure: sg
@@ -551,4 +552,11 @@
   |> add_syntax Syntax.pure_applC_syntax
   |> add_name "CPure";
 
+(**
+Emptiness-test for sorts: does there exist a type of sort 'sort' whose
+vars have sorts contained in 'sorts'?
+Trivial approximation at the moment.
+**)
+fun nonempty_sort(_,sorts,sort) = exists (fn s => sort subset s) sorts;
+
 end;