[isabelle-dev] Error with case syntax?
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Fri May 31 16:08:02 CEST 2013
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