src/Pure/term_ord.ML
changeset 80809 4a64fc4d1cde
parent 79096 48187f1a615e