Double quotes inside inner-syntax comment

Question

The " character, when placed inside a comment in a double-quoted piece of Isabelle's inner-syntax, does not behave as I would expect. To clarify: in the following function definition, I would expect the "at" sign to be parsed as a comment. In fact, Isabelle matches the first " character in the comment with the " at the start of that line, thus leading to a syntax error.

fun reverse where 
  "reverse [] = []"
| "reverse (x#xs) = reverse xs @ (* the "at" sign *) [x]"

I can work around this limitation by writing (* the 'at' sign *), but I'd rather understand what's really going on. So what's the right way to write this sort of comment inside an Isabelle term?

Answer 1

I suppose it would work with an escape character, like \" ?