src/Pure/General/binding.ML
changeset 56746 d37a5d09a277
parent 53380 08f3491c50bf
child 58032 e92cdae8b3b5