slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;
theory Syntax
imports Base
begin
chapter {* Concrete syntax and type-checking *}
text FIXME
section {* Parsing and printing *}
text FIXME
section {* Checking and unchecking \label{sec:term-check} *}
end