--- a/src/ZF/Tools/primrec_package.ML Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML Wed Aug 18 12:19:27 2010 +0200
@@ -115,8 +115,8 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const ("0", Ind_Syntax.iT),
- #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
+ (Const (@{const_name 0}, Ind_Syntax.iT),
+ #2 recursor_pair, Const (@{const_name 0}, 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))