1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -113,8 +113,8 @@
     1.4  
     1.5  fun remove_suc thy thms =
     1.6    let
     1.7 -    val vname = Name.variant (map fst
     1.8 -      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
     1.9 +    val vname = singleton (Name.variant_list (map fst
    1.10 +      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
    1.11      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    1.12      fun lhs_of th = snd (Thm.dest_comb
    1.13        (fst (Thm.dest_comb (cprop_of th))));
    1.14 @@ -166,8 +166,8 @@
    1.15  
    1.16  fun remove_suc_clause thy thms =
    1.17    let
    1.18 -    val vname = Name.variant (map fst
    1.19 -      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
    1.20 +    val vname = singleton (Name.variant_list (map fst
    1.21 +      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "x";
    1.22      fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
    1.23        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
    1.24        | find_var _ = NONE;