src/Pure/sign.ML

     val add_trrules: (string * string) trrule list -> sg -> sg
     val add_trrules_i: ast trrule list -> sg -> sg
     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
     val const_of_class: class -> string
     val class_of_const: string -> class

 
 val cpure = proto_pure
   |> 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;