src/Pure/General/binding.ML
changeset 70809 58677c92bef7
parent 70494 41108e3e9ca5
child 71212 475510f1a280