src/Pure/General/binding.ML
changeset 43425 0a5612040a8b
parent 42381 309ec68442c6
child 43546 6629e2dedb00