src/Pure/pattern.ML
changeset 1201 de2fc8cf9b6a
parent 1029 27808dabf4af
child 1435 aefcd255ed4a