src/Pure/pattern.ML
changeset 12902 a23dc0b7566f
parent 12826 dfb214fa310b
child 12980 8f717cbd4e44