src/Pure/type.ML
changeset 79394 2ff5ffd8731b
parent 79151 bf51996ba8c6
child 79395 40e3d97b277e
--- 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