src/Pure/pattern.ML
changeset 22720 296813d7d306
parent 22678 23963361278c
child 23222 daca4731942f