src/Pure/pattern.ML
changeset 2183 8d42a7bccf0b
parent 1576 af8f43f742a0
child 2227 18e993700540