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