src/Pure/pattern.ML
changeset 13800 16136d2da0db
parent 13645 430310b12c5b
child 13891 ae9a2a433388