diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Tue Jul 11 12:16:54 2006 +0200
@@ -153,7 +153,7 @@
 fun remove_suc thy thms =
   let
     val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
-    val vname = variant (map fst
+    val vname = Name.variant (map fst
       (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
     val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
     fun lhs_of th = snd (Thm.dest_comb
@@ -206,7 +206,7 @@
 fun remove_suc_clause thy thms =
   let
     val Suc_clause' = Thm.transfer thy Suc_clause;
-    val vname = variant (map fst
+    val vname = Name.variant (map fst
       (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
     fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)