# [isabelle] Adding a code equation for a class parameter

(Referring to both Isabelle2013 and Isabelle2013-1-RC2.)
Assume the following clone of the `nat` datatype and its obvious
instantiations for `zero` and `plus`, along with some auxiliary
definitions:
datatype natt = Z | S natt
instantiation natt :: "{zero,plus}" begin
definition zero_natt_def:
"0 = Z"
primrec plus_natt where
"Z + x = x" |
"(S m) + n = S (m + n)"
instance ..
end
fun f :: "'a::plus ⇒ 'a" where
"f x = x + x"
definition "i ≡ f (S Z)"
Now, exporting code for `i` works as expected, and
value [code] i
correctly yields `S (S Z)`.
However, if I add this code equation:
lemma [code]: "x + Z = x"
by (induct x) auto
... the generated code looks fishy (there is no warning of "subsumed code
equations" or the like):
export_code i in SML
fun plus_natta x Z = x;
Invoking `value [code] i` again produces an error:
Warning: Matches are not exhaustive.
fun plus_natta x Z = x
At (line 23 of "generated code")
Exception- Match raised
(Side note: `value [simp] i` fails to produce a normal form too, it just
prints `S Z + S Z`.)
I have no idea why that happens. Is what I'm trying to do even supported?
I couldn't find a hint in the type class tutorial (nor in the code
generation tutorial).

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*