src/Pure/pattern.ML
changeset 15517 3bc57d428ec1
parent 14981 e73f8140af78
child 15531 08c8dad8e399