src/Pure/pattern.ML
changeset 2773 36fdd908a26c
parent 2751 673c4eefd2e1
child 2792 6c17c5ec3d8b