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

[Alexander Krauss]

> What is the status of primrec anyway, in the light of fun(ction)?

It is still used
(a) for didactical reasons, to teach primitive recursion over datatypes,
(b) for bootstrapping purposes within HOL-Plain,
(c) since it is faster than fun, as it merely instantiates a combinator, and
(d) for higher-order datatypes (think Ordinals), which fun's automated 
termination provers cannot handle, since they only use measures into nat.

Alex