$print-short-symbol-names
special-variable
When true, symbol names are never printed with their package names.
make-html > $print-short-symbol-names it: false