src/Pure/pattern.ML
changeset 1000 0ad2b1da57ff
parent 678 6151b7f3b606
child 1029 27808dabf4af