src/HOL/Tools/old_primrec_package.ML
changeset 29276 94b1ffec9201
parent 29266 4a478f9d2847
child 29290 8fb767245822
--- a/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 19:54:03 2008 +0100
@@ -161,7 +161,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', (fnameTs'', fnss'')) =
                   (subst (map (fn ((x, y), z) =>
                                (Free x, (body_index y, Free z)))