# HG changeset patch
# User wenzelm
# Date 1703968500 -3600
# Node ID 2ff5ffd8731b2bb72f3c3e526f1f17593ff7fa6b
# Parent  0fb52d6ecb1be3e7bdeaea376eb43e2e79419357
clarified signature;

diff -r 0fb52d6ecb1b -r 2ff5ffd8731b src/HOL/Matrix_LP/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Sat Dec 30 21:22:31 2023 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Sat Dec 30 21:35:00 2023 +0100
@@ -297,7 +297,7 @@
               | HASKELL => ProgHaskell (AM_GHC.compile rules)
               | SML => ProgSML (AM_SML.compile rules)
 
-        fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
+        fun has_witness s = not (null (#1 (Sign.witness_sorts thy [] [s])))
 
         val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
 
@@ -345,7 +345,7 @@
         val shyptab = add_shyps shyps Sorttab.empty
         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
         fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
-        fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
+        fun has_witness s = not (null (#1 (Sign.witness_sorts thy [] [s])))
         val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
         val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
         val _ =
diff -r 0fb52d6ecb1b -r 2ff5ffd8731b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Dec 30 21:22:31 2023 +0100
+++ b/src/Pure/sign.ML	Sat Dec 30 21:35:00 2023 +0100
@@ -23,7 +23,8 @@
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
   val inter_sort: theory -> sort * sort -> sort
-  val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
+  val witness_sorts: theory -> (typ * sort) list -> sort Ord_List.T ->
+    (typ * sort) list * sort Ord_List.T
   val logical_types: theory -> string list
   val typ_instance: theory -> typ * typ -> bool
   val typ_equiv: theory -> typ * typ -> bool
diff -r 0fb52d6ecb1b -r 2ff5ffd8731b src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Dec 30 21:22:31 2023 +0100
+++ b/src/Pure/sorts.ML	Sat Dec 30 21:35:00 2023 +0100
@@ -64,7 +64,8 @@
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
   val classrel_derivation: algebra ->
     ('a * class -> class -> 'a) -> 'a * class -> class -> 'a  (*exception CLASS_ERROR*)
-  val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
+  val witness_sorts: algebra -> string list -> (typ * sort) list -> sort Ord_List.T ->
+    (typ * sort) list * sort Ord_List.T
 end;
 
 structure Sorts: SORTS =
@@ -489,6 +490,8 @@
                 end
           | NONE => witn_types path ts S solved_failed);
 
-  in map_filter I (#1 (witn_sorts [] sorts ([], []))) end;
+    val witnessed = map_filter I (#1 (witn_sorts [] sorts ([], [])));
+    val non_witnessed = fold (remove_sort o #2) witnessed sorts;
+  in (witnessed, non_witnessed) end;
 
 end;
diff -r 0fb52d6ecb1b -r 2ff5ffd8731b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 30 21:22:31 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 30 21:35:00 2023 +0100
@@ -1058,9 +1058,7 @@
         val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
 
         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)];
@@ -1070,8 +1068,8 @@
         val present = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present_set);
 
         val extra = fold (Sorts.remove_sort o #2) present shyps;
-        val witnessed = Sign.witness_sorts thy present extra;
-        val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);
+        val (witnessed, non_witnessed) =
+          Sign.witness_sorts thy present extra ||> map (`(Sorts.minimize_sort algebra));
 
         val extra' =
           non_witnessed |> map_filter (fn (S, _) =>
diff -r 0fb52d6ecb1b -r 2ff5ffd8731b src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Dec 30 21:22:31 2023 +0100
+++ b/src/Pure/type.ML	Sat Dec 30 21:35:00 2023 +0100
@@ -38,7 +38,8 @@
   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
+  val witness_sorts: tsig -> (typ * sort) list -> sort Ord_List.T ->
+    (typ * sort) list * sort Ord_List.T
   type mode
   val mode_default: mode
   val mode_syntax: mode