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

_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to