[isabelle-dev] Error with case syntax?

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri May 31 16:08:02 CEST 2013

Hi all,

Using Isabelle/c3f837d92537,

    theory Bug imports Main begin

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


    *** 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.



More information about the isabelle-dev mailing list