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)))