# HG changeset patch
# User wenzelm
# Date 809953999 -7200
# Node ID 2c0d94151e749c69508ef2d331f9c9716723746b
# Parent  289c573327f026251b078030fd15b5e6464769da
nonempty_sort: no longer var names as args;

diff -r 289c573327f0 -r 2c0d94151e74 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Sep 01 13:11:09 1995 +0200
+++ b/src/Pure/sign.ML	Fri Sep 01 13:13:19 1995 +0200
@@ -25,7 +25,7 @@
     val classes: sg -> class list
     val subsort: sg -> sort * sort -> bool
     val norm_sort: sg -> sort -> sort
-    val nonempty_sort: sg -> (string * sort) list -> sort -> bool
+    val nonempty_sort: sg -> sort list -> sort -> bool
     val print_sg: sg -> unit
     val pretty_sg: sg -> Pretty.T
     val pprint_sg: sg -> pprint_args -> unit
@@ -193,7 +193,7 @@
 
 fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
 
-fun string_of_term (Sg {syn, stamps, ...}) = 
+fun string_of_term (Sg {syn, stamps, ...}) =
   let val curried = "CPure" mem (map ! stamps);
   in Syntax.string_of_term curried syn end;
 
@@ -266,7 +266,7 @@
 
     fun term_err [] = ""
       | term_err [t] = "\nInvolving this term:\n" ^ show_term t
-      | term_err ts = 
+      | term_err ts =
           "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
 
     fun exn_type_msg (msg, Ts, ts) =
diff -r 289c573327f0 -r 2c0d94151e74 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Sep 01 13:11:09 1995 +0200
+++ b/src/Pure/type.ML	Fri Sep 01 13:13:19 1995 +0200
@@ -38,7 +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 nonempty_sort: type_sig -> sort list -> sort -> bool
   val cert_typ: type_sig -> typ -> typ
   val norm_typ: type_sig -> typ -> typ
   val freeze: term -> term
@@ -406,7 +406,7 @@
 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;
+        orelse exists (fn S' => subsort tsig (S', S)) hyps;