[isabelle-dev] fun f where "f 0 = ..." raises TYPE

[Tjark Weber]

Hi,

Attempting to define

  fun f where "f 0 = undefined"

in Isabelle/HOL (7f2793d51efc) yields

*** exception TYPE raised (line 38 of
".../isabelle/src/HOL/Tools/Function/pattern_split.ML"): inst_constrs_of
*** At command "fun"

A more user-friendly error message would be nice.

Kind regards,
Tjark