[isabelle-dev] unhelpful low-level error message from primrec

[Brian Huffman]

Hello all,

I just noticed this error message from primrec if you write a
specification that is not primitive recursive. Here is a simplified
example:

primrec foo :: "nat => nat" where
  "foo 0 = 1" | "foo (Suc n) = foo 0"

*** Extra variables on rhs: "foo"
*** The error(s) above occurred in definition "foo_def":
***   "foo \<equiv> \<lambda>a. nat_rec 1 (\<lambda>n na. foo 0) a"
*** At command "primrec"

Apparently, the primrec package gets as far as trying to register the
non-recursive definition; then the definition command fails, and the
error is not caught by primrec.

It might be nice to generate a more helpful error message in this
case, instead of one that originates from a lower-level tool.

- Brian