src/Pure/pattern.ML
changeset 14010 32faa7e2e767
parent 13998 75a399c2781f
child 14643 130076a81b84