src/Pure/Syntax/local_syntax.ML
changeset 80659 2191ad2d684e
parent 80074 951c371c1cd9
child 80897 5328d67ec647