[isabelle-dev] Error with case syntax?

[Jasmin Christian Blanchette]

Hi all,

Using Isabelle/c3f837d92537,

    theory Bug imports Main begin

    lemma "(case p of (a, b) => f (a, b)) = f p"

raises

    *** exception TERM raised (line 332 of "term.ML"): fastype_of: expected function type

in Proof General and in "isabelle tty" but not in jEdit.

Needless to say, the statement is legitimate and used to work with earlier versions. I have no idea what is going on here.

Cheers,

Jasmin