src/Pure/pattern.ML
changeset 2348 b51e104ecf40
parent 2227 18e993700540
child 2616 704b6c7432cf