--- a/src/ZF/Tools/primrec_package.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/primrec_package.ML Mon Dec 20 16:44:33 2010 +0100
@@ -115,8 +115,8 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const (@{const_name 0}, Ind_Syntax.iT),
- #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
+ (Const (@{const_name zero}, Ind_Syntax.iT),
+ #2 recursor_pair, Const (@{const_name zero}, Ind_Syntax.iT)))
| SOME (rhs, cargs', eq) =>
(rhs, inst_recursor (recursor_pair, cargs'), eq)
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))