src/Pure/pattern.ML
changeset 2495 82ec47e0a8d3
parent 2227 18e993700540
child 2616 704b6c7432cf