changeset 79395 | 40e3d97b277e |
parent 79394 | 2ff5ffd8731b |
child 79411 | 700d4f16b5f2 |
--- 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