changeset 70586 | 57df8a85317a |
parent 66301 | 8a6a89d6cf2b |
child 72966 | f931a2a68ab8 |
--- a/src/Tools/Argo/argo_proof.ML Tue Aug 20 09:48:22 2019 +0200 +++ b/src/Tools/Argo/argo_proof.ML Tue Aug 20 11:01:05 2019 +0200 @@ -52,7 +52,7 @@ (* equalities and orders *) val eq_proof_id: proof_id * proof_id -> bool - val proof_id_ord: proof_id * proof_id -> order + val proof_id_ord: proof_id ord (* conversion constructors *) val keep_conv: conv