Argh, some kind of clash with Ott's LaTeX output over "comp".
Formatting
Not terribly nice Isabelle proof that "bad" needs alpha-conversion.