src/Pure/pattern.ML
changeset 3684 f677f0bc1cdf
parent 2792 6c17c5ec3d8b
child 4667 6328d427a339