src/Pure/General/binding.ML
changeset 62337 d3996d5873dd
parent 62241 a4a1f282bcd5
child 62663 bea354f6ff21