--- 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;