diff -r 660234d959f7 -r bce03c644efb src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Dec 30 21:46:14 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Dec 30 21:46:48 2008 +0100
@@ -127,7 +127,7 @@
 fun remove_suc thy thms =
   let
     val vname = Name.variant (map fst
-      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
+      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
     val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
     fun lhs_of th = snd (Thm.dest_comb
       (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
@@ -180,7 +180,7 @@
 fun remove_suc_clause thy thms =
   let
     val vname = Name.variant (map fst
-      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
+      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
     fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
       | find_var _ = NONE;