src/Pure/pattern.ML
changeset 16510 606d919ad3c3
parent 15797 a63605582573
child 16651 40b96a501773