tsig: removed unnecessary universal witness;
authorwenzelm
Sun Apr 13 16:40:02 2008 +0200 (2008-04-13)
changeset 266370bfccafc52eb
parent 26636 65343a5ac627
child 26638 1d5d42d8fd66
tsig: removed unnecessary universal witness;
src/Pure/display.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/display.ML	Sun Apr 13 14:30:23 2008 +0200
     1.2 +++ b/src/Pure/display.ML	Sun Apr 13 16:40:02 2008 +0200
     1.3 @@ -148,11 +148,6 @@
     1.4      fun pretty_default S = Pretty.block
     1.5        [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
     1.6  
     1.7 -    fun pretty_witness NONE = Pretty.str "universal non-emptiness witness: -"
     1.8 -      | pretty_witness (SOME (T, S)) = Pretty.block
     1.9 -          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1,
    1.10 -            prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S];
    1.11 -
    1.12      val tfrees = map (fn v => TFree (v, []));
    1.13      fun pretty_type syn (t, (Type.LogicalType n, _)) =
    1.14            if syn then NONE
    1.15 @@ -189,7 +184,7 @@
    1.16      val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
    1.17      val {constants, constraints} = Consts.dest consts;
    1.18      val extern_const = NameSpace.extern (#1 constants);
    1.19 -    val {classes, default, types, witness, ...} = Type.rep_tsig tsig;
    1.20 +    val {classes, default, types, ...} = Type.rep_tsig tsig;
    1.21      val (class_space, class_algebra) = classes;
    1.22      val {classes, arities} = Sorts.rep_algebra class_algebra;
    1.23  
    1.24 @@ -221,7 +216,6 @@
    1.25      [Pretty.strs ["name prefix:", NameSpace.path_of naming],
    1.26        Pretty.big_list "classes:" (map pretty_classrel clsses),
    1.27        pretty_default default,
    1.28 -      pretty_witness witness,
    1.29        Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
    1.30        Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
    1.31        Pretty.big_list "type arities:" (pretty_arities arties),
     2.1 --- a/src/Pure/sign.ML	Sun Apr 13 14:30:23 2008 +0200
     2.2 +++ b/src/Pure/sign.ML	Sun Apr 13 16:40:02 2008 +0200
     2.3 @@ -78,8 +78,6 @@
     2.4    val subsort: theory -> sort * sort -> bool
     2.5    val of_sort: theory -> typ * sort -> bool
     2.6    val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
     2.7 -  val universal_witness: theory -> (typ * sort) option
     2.8 -  val all_sorts_nonempty: theory -> bool
     2.9    val is_logtype: theory -> string -> bool
    2.10    val typ_instance: theory -> typ * typ -> bool
    2.11    val typ_equiv: theory -> typ * typ -> bool
    2.12 @@ -235,7 +233,6 @@
    2.13  
    2.14  val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
    2.15  val all_classes = Sorts.all_classes o classes_of;
    2.16 -val minimal_classes = Sorts.minimal_classes o classes_of;
    2.17  val super_classes = Sorts.super_classes o classes_of;
    2.18  val minimize_sort = Sorts.minimize_sort o classes_of;
    2.19  val complete_sort = Sorts.complete_sort o classes_of;
    2.20 @@ -244,8 +241,6 @@
    2.21  val subsort = Type.subsort o tsig_of;
    2.22  val of_sort = Type.of_sort o tsig_of;
    2.23  val witness_sorts = Type.witness_sorts o tsig_of;
    2.24 -val universal_witness = Type.universal_witness o tsig_of;
    2.25 -val all_sorts_nonempty = is_some o universal_witness;
    2.26  val is_logtype = member (op =) o Type.logical_types o tsig_of;
    2.27  
    2.28  val typ_instance = Type.typ_instance o tsig_of;