--- a/src/Pure/sign.ML Sat Dec 30 21:35:00 2023 +0100
+++ b/src/Pure/sign.ML Sat Dec 30 21:40:48 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 Ord_List.T ->
+ 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
--- a/src/Pure/sorts.ML Sat Dec 30 21:35:00 2023 +0100
+++ b/src/Pure/sorts.ML Sat Dec 30 21:40:48 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 Ord_List.T ->
+ val witness_sorts: algebra -> string list ->
+ (typ * sort) list -> sort Ord_List.T ->
(typ * sort) list * sort Ord_List.T
end;
--- a/src/Pure/type.ML Sat Dec 30 21:35:00 2023 +0100
+++ b/src/Pure/type.ML Sat Dec 30 21:40:48 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 Ord_List.T ->
+ val witness_sorts: tsig ->
+ (typ * sort) list -> sort Ord_List.T ->
(typ * sort) list * sort Ord_List.T
type mode
val mode_default: mode