Function parse_theorem_in 

pub fn parse_theorem_in(
    ctx: &Context,
    input: &str,
) -> Result<(Command, usize), ParseError>

parse_theorem, with the kernel context.

The one thing it buys is the one thing text cannot carry: the constructor list of whatever induction <v> is eliminating. With it, a bullet-count mistake is reported AS a bullet-count mistake — naming the inductive, its constructors and the count written — instead of arriving as “the tactic did not establish the stated goal”, which is what a reader sees when the case chain is silently the wrong length.