# HG changeset patch
# User wenzelm
# Date 1581968104 -3600
# Node ID b2c9f94e025f7eccbbddb6e369d4aaa09b3385c8
# Parent  fb08117a106ba1a7a791983f705caccb9a51aea9
proper sort constraints for strip_shyps, for sort relations used in minimization;

diff -r fb08117a106b -r b2c9f94e025f src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Feb 17 11:17:09 2020 +0100
+++ b/src/Pure/sorts.ML	Mon Feb 17 20:35:04 2020 +0100
@@ -37,7 +37,6 @@
   val inter_sort: algebra -> sort * sort -> sort
   val minimize_sort: algebra -> sort -> sort
   val complete_sort: algebra -> sort -> sort
-  val minimal_sorts: algebra -> sort list -> sort Ord_List.T
   val add_class: Context.generic -> class * class list -> algebra -> algebra
   val add_classrel: Context.generic -> class * class -> algebra -> algebra
   val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra
@@ -177,12 +176,6 @@
 fun complete_sort algebra =
   Graph.all_succs (classes_of algebra) o minimize_sort algebra;
 
-fun minimal_sorts algebra raw_sorts =
-  let
-    fun le S1 S2 = sort_le algebra (S1, S2);
-    val sorts = make (map (minimize_sort algebra) raw_sorts);
-  in sorts |> filter_out (fn S => exists (fn S' => le S' S andalso not (le S S')) sorts) end;
-
 
 
 (** build algebras **)
diff -r fb08117a106b -r b2c9f94e025f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Feb 17 11:17:09 2020 +0100
+++ b/src/Pure/thm.ML	Mon Feb 17 20:35:04 2020 +0100
@@ -1700,14 +1700,29 @@
   | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) =>
       let
         val thy = theory_of_thm thm;
+
         val algebra = Sign.classes_of thy;
+        val minimize = Sorts.minimize_sort algebra;
+        val le = Sorts.sort_le algebra;
+        fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
+        fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
 
         val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
         val extra = fold (Sorts.remove_sort o #2) present shyps;
         val witnessed = Sign.witness_sorts thy present extra;
-        val extra' = fold (Sorts.remove_sort o #2) witnessed extra
-          |> Sorts.minimal_sorts algebra;
-        val constraints' = fold (insert_constraints thy) witnessed constraints;
+        val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
+
+        val extra' =
+          non_witnessed |> map_filter (fn (S, _) =>
+            if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S)
+          |> Sorts.make;
+
+        val constrs' =
+          non_witnessed |> maps (fn (S1, S2) =>
+            let val S0 = the (find_first (fn S => le (S, S1)) extra')
+            in rel (S0, S1) @ rel (S1, S2) end);
+
+        val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints;
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
       in
         Thm (deriv_rule_unconditional