export Type.minimize_sort;

--- a/src/Pure/type.ML	Wed Apr 28 08:25:02 2010 +0200
+++ b/src/Pure/type.ML	Wed Apr 28 10:43:08 2010 +0200
@@ -32,6 +32,7 @@
   val inter_sort: tsig -> sort * sort -> sort
   val cert_class: tsig -> class -> class
   val cert_sort: tsig -> sort -> sort
+  val minimize_sort: tsig -> sort -> sort
   val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list
   type mode
   val mode_default: mode
@@ -159,6 +160,7 @@
 
 fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
 fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
+fun minimize_sort (TSig {classes, ...}) = Sorts.minimize_sort (#2 classes);
 
 fun witness_sorts (TSig {classes, log_types, ...}) =
   Sorts.witness_sorts (#2 classes) log_types;