src/Pure/General/binding.ML
changeset 65751 426d4bf3b9bb
parent 63369 4698dd1106ae
child 70494 41108e3e9ca5