src/HOL/Nominal/nominal_inductive2.ML

           REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
           REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
   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 =
   let val env = Pattern.first_order_match thy (p, prop_of th)
     (Vartab.empty, Vartab.empty)