prefer attributes antiquotation over Attrib.internal;
adapted to Isabelle/bc42c074e58f;