# HG changeset patch
# User wenzelm
# Date 1272397570 -7200
# Node ID 9d6b3be996d4f405a2ab1d26ad7fe45c86ad9e92
# Parent  874843c1e96eea322f88c3d57809b369d248bad7
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;

diff -r 874843c1e96e -r 9d6b3be996d4 NEWS
--- a/NEWS	Tue Apr 27 21:34:22 2010 +0200
+++ b/NEWS	Tue Apr 27 21:46:10 2010 +0200
@@ -295,6 +295,14 @@
 
 *** ML ***
 
+* Sorts.certify_sort and derived "cert" operations for types and terms
+no longer minimize sorts.  Thus certification at the boundary of the
+inference kernel becomes invariant under addition of class relations,
+which is an important monotonicity principle.  Sorts are now minimized
+in the syntax layer only, at the boundary between the end-user and the
+system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
+explicitly in rare situations.
+
 * Antiquotations for basic formal entities:
 
     @{class NAME}         -- type class
diff -r 874843c1e96e -r 9d6b3be996d4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 27 21:34:22 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 27 21:46:10 2010 +0200
@@ -610,6 +610,7 @@
 
 fun get_sort ctxt raw_env =
   let
+    val thy = theory_of ctxt;
     val tsig = tsig_of ctxt;
 
     fun eq ((xi, S), (xi', S')) =
@@ -636,7 +637,7 @@
           else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
             " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
             " for type variable " ^ quote (Term.string_of_vname' xi)));
-  in get end;
+  in Sign.minimize_sort thy o get end;
 
 fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi);
 fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S));
@@ -736,10 +737,11 @@
 
 fun parse_sort ctxt text =
   let
+    val thy = theory_of ctxt;
     val (syms, pos) = Syntax.parse_token Markup.sort text;
     val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
       handle ERROR msg => cat_error msg  ("Failed to parse sort" ^ Position.str_of pos)
-  in S end;
+  in Sign.minimize_sort thy S end;
 
 fun parse_typ ctxt text =
   let
diff -r 874843c1e96e -r 9d6b3be996d4 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Tue Apr 27 21:34:22 2010 +0200
+++ b/src/Pure/sorts.ML	Tue Apr 27 21:46:10 2010 +0200
@@ -189,7 +189,7 @@
   if can (Graph.get_node (classes_of algebra)) c then c
   else raise TYPE ("Undeclared class: " ^ quote c, [], []);
 
-fun certify_sort classes = minimize_sort classes o map (certify_class classes);
+fun certify_sort classes = map (certify_class classes);