src/Pure/Syntax/local_syntax.ML
changeset 81543 fa37ee54644c
parent 81149 0e506128c14a
child 81591 d570d215e380