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