static S tok_dropAsterisks(S s) {
  ret join(replace(javaTok(s), "*", ""));
}