# HG changeset patch
# User wenzelm
# Date 1272444188 -7200
# Node ID c311bd68f9190045b5f18f2c44cab5ad0f9048d5
# Parent  06081e4921d618fe374022c4ed0988d35408b22c
export Type.minimize_sort;

diff -r 06081e4921d6 -r c311bd68f919 src/Pure/type.ML
--- 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;