src/Pure/Tools/class_deps.ML
changeset 67331 a8770603a269
parent 62848 e4140efe699e