src/Pure/General/binding.ML
changeset 59527 edaabc1ab1ed
parent 58032 e92cdae8b3b5
child 59858 890b68e1e8b6