# HG changeset patch
# User wenzelm
# Date 1208097602 -7200
# Node ID 0bfccafc52ebd6f248e3a1153849efeea6adc5b8
# Parent  65343a5ac627e36e7a341c892367fd1f2625188c
tsig: removed unnecessary universal witness;

diff -r 65343a5ac627 -r 0bfccafc52eb src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Apr 13 14:30:23 2008 +0200
+++ b/src/Pure/display.ML	Sun Apr 13 16:40:02 2008 +0200
@@ -148,11 +148,6 @@
     fun pretty_default S = Pretty.block
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
-    fun pretty_witness NONE = Pretty.str "universal non-emptiness witness: -"
-      | pretty_witness (SOME (T, S)) = Pretty.block
-          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1,
-            prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S];
-
     val tfrees = map (fn v => TFree (v, []));
     fun pretty_type syn (t, (Type.LogicalType n, _)) =
           if syn then NONE
@@ -189,7 +184,7 @@
     val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
     val {constants, constraints} = Consts.dest consts;
     val extern_const = NameSpace.extern (#1 constants);
-    val {classes, default, types, witness, ...} = Type.rep_tsig tsig;
+    val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
     val {classes, arities} = Sorts.rep_algebra class_algebra;
 
@@ -221,7 +216,6 @@
     [Pretty.strs ["name prefix:", NameSpace.path_of naming],
       Pretty.big_list "classes:" (map pretty_classrel clsses),
       pretty_default default,
-      pretty_witness witness,
       Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
       Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
       Pretty.big_list "type arities:" (pretty_arities arties),
diff -r 65343a5ac627 -r 0bfccafc52eb src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Apr 13 14:30:23 2008 +0200
+++ b/src/Pure/sign.ML	Sun Apr 13 16:40:02 2008 +0200
@@ -78,8 +78,6 @@
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
   val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
-  val universal_witness: theory -> (typ * sort) option
-  val all_sorts_nonempty: theory -> bool
   val is_logtype: theory -> string -> bool
   val typ_instance: theory -> typ * typ -> bool
   val typ_equiv: theory -> typ * typ -> bool
@@ -235,7 +233,6 @@
 
 val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
 val all_classes = Sorts.all_classes o classes_of;
-val minimal_classes = Sorts.minimal_classes o classes_of;
 val super_classes = Sorts.super_classes o classes_of;
 val minimize_sort = Sorts.minimize_sort o classes_of;
 val complete_sort = Sorts.complete_sort o classes_of;
@@ -244,8 +241,6 @@
 val subsort = Type.subsort o tsig_of;
 val of_sort = Type.of_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
-val universal_witness = Type.universal_witness o tsig_of;
-val all_sorts_nonempty = is_some o universal_witness;
 val is_logtype = member (op =) o Type.logical_types o tsig_of;
 
 val typ_instance = Type.typ_instance o tsig_of;