src/Pure/pattern.ML
changeset 78659 b5f3d1051b13
parent 70443 a21a96eda033
child 80910 406a85a25189