src/Pure/pattern.ML
changeset 5840 e2d2b896c717
parent 4820 8f6dbbd8d497
child 6539 2e7d2fba9f6c