--- a/src/HOL/Nominal/nominal_primrec.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Dec 31 19:54:03 2008 +0100
@@ -155,7 +155,7 @@
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map fst recs;
val subs = map (rpair dummyT o fst)
- (rev (rename_wrt_term rhs rargs));
+ (rev (Term.rename_wrt_term rhs rargs));
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle RecError s => primrec_eq_err lthy s eq