1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Dec 30 21:46:14 2008 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Dec 30 21:46:48 2008 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4  fun remove_suc thy thms =
     1.5    let
     1.6      val vname = Name.variant (map fst
     1.7 -      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
     1.8 +      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
     1.9      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    1.10      fun lhs_of th = snd (Thm.dest_comb
    1.11        (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
    1.12 @@ -180,7 +180,7 @@
    1.13  fun remove_suc_clause thy thms =
    1.14    let
    1.15      val vname = Name.variant (map fst
    1.16 -      (fold (Term.add_varnames o Thm.full_prop_of) thms [])) "x";
    1.17 +      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
    1.18      fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
    1.19        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
    1.20        | find_var _ = NONE;