theory Xxxxx imports Pure keywords "yyyyy" :: prf_open begin ML \ @{keyword "("} : string parser; (* this works as expected *) val _ = Outer_Syntax.command @{command_keyword yyyyy} "dummy definition yyyyy" (Scan.succeed (Toplevel.proof Proof.begin_block)); @{keyword "yyyyy"}; (*ERROR Bad outer syntax keyword "yyyyy"*) \ end