diff -r 9fa69e3858d6 -r 94b1ffec9201 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 19:54:03 2008 +0100
@@ -138,7 +138,7 @@
   in Option.map prove (map_term f prop (the_default prop opt)) end;
 
 fun abs_params params t =
-  let val vs =  map (Var o apfst (rpair 0)) (rename_wrt_term t params)
+  let val vs =  map (Var o apfst (rpair 0)) (Term.rename_wrt_term t params)
   in (list_all (params, t), (rev vs, subst_bounds (vs, t))) end;
 
 fun inst_params thy (vs, p) th cts =