# HG changeset patch
# User nipkow
# Date 807273365 -7200
# Node ID 3f3888213ceb1dae296769af2a6c11a7dda25a82
# Parent  a8f6d0fa2a59f15379131f966f690d647c78e2ce
Added nonempty_sort.

diff -r a8f6d0fa2a59 -r 3f3888213ceb src/Pure/sign.ML
--- 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;