src/Pure/pattern.ML
changeset 18679 cf9f1584431a
parent 18182 786d83044780
child 18940 d8e12bf337a3