src/Pure/morphism.ML
changeset 80879 fb1dd189c4f3
parent 80809 4a64fc4d1cde