src/Pure/Tools/thy_deps.ML
changeset 83053 c1ccd17fb70f
parent 82598 766a07ff7a07