locals.scm used bare @local.definition instead of the required @local.definition.<class> suffix, so its captures had no effect. highlights.scm used @function.definition and @function.call, which aren't real highlight scopes (they fall back to plain @function anyway). Fixed both to follow convention, splitting locals.scm definitions into variable (floating/essential hypotheses) and function (axiom/provable theorems) to match the classification already used in tags.scm. Co-authored-by: m4dh0rs3 <54140937+m4dh0rs3@users.noreply.github.com>