src/Pure/search.ML
changeset 70690 8518a750f7bb
parent 62919 9eb0359d6a77