src/Pure/sign.ML
changeset 26637 0bfccafc52eb
parent 26631 d6b6c74a8bcf
child 26667 660b69b3c28a
     1.1 --- a/src/Pure/sign.ML	Sun Apr 13 14:30:23 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Apr 13 16:40:02 2008 +0200
     1.3 @@ -78,8 +78,6 @@
     1.4    val subsort: theory -> sort * sort -> bool
     1.5    val of_sort: theory -> typ * sort -> bool
     1.6    val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
     1.7 -  val universal_witness: theory -> (typ * sort) option
     1.8 -  val all_sorts_nonempty: theory -> bool
     1.9    val is_logtype: theory -> string -> bool
    1.10    val typ_instance: theory -> typ * typ -> bool
    1.11    val typ_equiv: theory -> typ * typ -> bool
    1.12 @@ -235,7 +233,6 @@
    1.13  
    1.14  val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
    1.15  val all_classes = Sorts.all_classes o classes_of;
    1.16 -val minimal_classes = Sorts.minimal_classes o classes_of;
    1.17  val super_classes = Sorts.super_classes o classes_of;
    1.18  val minimize_sort = Sorts.minimize_sort o classes_of;
    1.19  val complete_sort = Sorts.complete_sort o classes_of;
    1.20 @@ -244,8 +241,6 @@
    1.21  val subsort = Type.subsort o tsig_of;
    1.22  val of_sort = Type.of_sort o tsig_of;
    1.23  val witness_sorts = Type.witness_sorts o tsig_of;
    1.24 -val universal_witness = Type.universal_witness o tsig_of;
    1.25 -val all_sorts_nonempty = is_some o universal_witness;
    1.26  val is_logtype = member (op =) o Type.logical_types o tsig_of;
    1.27  
    1.28  val typ_instance = Type.typ_instance o tsig_of;