# HG changeset patch
# User wenzelm
# Date 807290269 -7200
# Node ID a206f722bef97c6993ca7bc7a8d749f71739e049
# Parent  3f3888213ceb1dae296769af2a6c11a7dda25a82
added nonempty_sort (a somewhat braindead version!);

diff -r 3f3888213ceb -r a206f722bef9 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Aug 01 12:36:05 1995 +0200
+++ b/src/Pure/type.ML	Tue Aug 01 17:17:49 1995 +0200
@@ -38,6 +38,7 @@
   val subsort: type_sig -> sort * sort -> bool
   val norm_sort: type_sig -> sort -> sort
   val rem_sorts: typ -> typ
+  val nonempty_sort: type_sig -> (string * sort) list -> sort -> bool
   val cert_typ: type_sig -> typ -> typ
   val norm_typ: type_sig -> typ -> typ
   val freeze: term -> term
@@ -399,6 +400,16 @@
   | rem_sorts (TVar (xi, _)) = TVar (xi, []);
 
 
+(* nonempty_sort *)
+
+(* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *)
+fun nonempty_sort _ _ [] = true
+  | nonempty_sort (tsig as TySg {arities, ...}) hyps S =
+      exists (exists (fn (c, ss) => [c] = S andalso null ss) o snd) arities
+        orelse exists (fn (_, S') => subsort tsig (S', S)) hyps;
+
+
+
 (* typ_errors *)
 
 (*check validity of (not necessarily normal) type; accumulate error messages*)