# HG changeset patch
# User wenzelm
# Date 1307630089 -7200
# Node ID 2b47822868e41f9e78c5ae81aced61259d176e0b
# Parent  28e71a685c84b129ccf4c7482b3d42e49b49d2fc
discontinued Name.variant to emphasize that this is old-style / indirect;

diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -403,7 +403,7 @@
 
     (* calculate function arguments of case combinator *)
     val tns = map fst (Term.add_tfreesT lhsT [])
-    val resultT = TFree (Name.variant tns "'t", @{sort pcpo})
+    val resultT = TFree (singleton (Name.variant_list tns) "'t", @{sort pcpo})
     fun fTs T = map (fn (_, args) => map snd args -->> T) spec
     val fns = Datatype_Prop.indexify_names (map (K "f") spec)
     val fs = map Free (fns ~~ fTs resultT)
@@ -768,7 +768,7 @@
     val resultT : typ =
       let
         val ts : string list = map fst (Term.add_tfreesT lhsT [])
-        val t : string = Name.variant ts "'t"
+        val t : string = singleton (Name.variant_list ts) "'t"
       in TFree (t, @{sort pcpo}) end
 
     (* define match combinators *)
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -234,7 +234,7 @@
           in comp_con T f rhs' (v::vs) taken' end
       | Const (c, cT) =>
           let
-            val n = Name.variant taken "v"
+            val n = singleton (Name.variant_list taken) "v"
             val v = Free(n, T)
             val m = Const(match_name c, matcherT (cT, fastype_of rhs))
             val k = big_lambdas vs rhs
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Thu Jun 09 16:34:49 2011 +0200
@@ -531,7 +531,7 @@
     (* prove strictness and reduction rules of pattern combinators *)
     local
       val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
-      val rn = Name.variant tns "'r";
+      val rn = singleton (Name.variant_list tns) "'r";
       val R = TFree (rn, @{sort pcpo});
       fun pat_lhs (pat, args) =
         let
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jun 09 16:34:49 2011 +0200
@@ -618,7 +618,6 @@
 open Code_Thingol;
 
 fun imp_program naming =
-
   let
     fun is_const c = case lookup_const naming c
      of SOME c' => (fn c'' => c' = c'')
@@ -635,7 +634,7 @@
       | dest_abs (t, ty) =
           let
             val vs = fold_varnames cons t [];
-            val v = Name.variant vs "x";
+            val v = singleton (Name.variant_list vs) "x";
             val ty' = (hd o fst o unfold_fun) ty;
           in ((SOME v, ty'), t `$ IVar (SOME v)) end;
     fun force (t as IConst (c, _) `$ t') = if is_return c
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Import/hol4rews.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -605,7 +605,7 @@
                 then F defname                 (* name_def *)
                 else if not (member (op =) used pdefname)
                 then F pdefname                (* name_primdef *)
-                else F (Name.variant used pdefname) (* last resort *)
+                else F (singleton (Name.variant_list used) pdefname) (* last resort *)
             end
     end
 
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -228,7 +228,7 @@
         val (type_inst,_) =
             fold (fn (w as (v,_), S) => fn (inst, used) =>
                       let
-                          val v' = Name.variant used v
+                          val v' = singleton (Name.variant_list used) v
                       in
                           ((w,TFree(v',S))::inst,v'::used)
                       end)
@@ -298,7 +298,7 @@
               then
                   let
                       val cert = cterm_of thy
-                      val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
+                      val v = Free (singleton (Name.variant_list (Term.add_free_names t [])) "v", xT)
                       val cv = cert v
                       val ct = cert t
                       val th = (Thm.assume ct)
@@ -361,7 +361,7 @@
                       Type("fun",[aT,bT]) =>
                       let
                           val cert = cterm_of thy
-                          val vname = Name.variant (Term.add_free_names t []) "v"
+                          val vname = singleton (Name.variant_list (Term.add_free_names t [])) "v"
                           val v = Free(vname,aT)
                           val cv = cert v
                           val ct = cert t
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Inductive.thy	Thu Jun 09 16:34:49 2011 +0200
@@ -295,7 +295,8 @@
 let
   fun fun_tr ctxt [cs] =
     let
-      val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
+      (* FIXME proper name context!? *)
+      val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
       val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
     in lambda x ft end
 in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jun 09 16:34:49 2011 +0200
@@ -113,8 +113,8 @@
 
 fun remove_suc thy thms =
   let
-    val vname = Name.variant (map fst
-      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
+    val vname = singleton (Name.variant_list (map fst
+      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
     val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
     fun lhs_of th = snd (Thm.dest_comb
       (fst (Thm.dest_comb (cprop_of th))));
@@ -166,8 +166,8 @@
 
 fun remove_suc_clause thy thms =
   let
-    val vname = Name.variant (map fst
-      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
+    val vname = singleton (Name.variant_list (map fst
+      (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;
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/List.thy	Thu Jun 09 16:34:49 2011 +0200
@@ -383,7 +383,8 @@
 
   fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
     let
-      val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
+      (* FIXME proper name context!? *)
+      val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
       val e = if opti then singl e else e;
       val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
       val case2 =
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -622,7 +622,7 @@
               (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
         let
           val permT = mk_permT
-            (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
+            (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
           val pi = Free ("pi", permT);
           val T = Type (Sign.intern_type thy name, map TFree tvs);
         in apfst (pair r o hd)
@@ -1169,7 +1169,7 @@
         val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
         val frees' = partition_cargs idxs frees;
-        val z = (Name.variant tnames "z", fsT);
+        val z = (singleton (Name.variant_list tnames) "z", fsT);
 
         fun mk_prem ((dt, s), T) =
           let
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -207,7 +207,7 @@
 fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) =
   let
     val used = map fst (fold Term.add_frees fs []);
-    val x = (Name.variant used "x", dummyT);
+    val x = (singleton (Name.variant_list used) "x", dummyT);
     val frees = ls @ x :: rs;
     val raw_rhs = list_abs_free (frees,
       list_comb (Const (rec_name, dummyT), fs @ [Free x]))
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -379,8 +379,8 @@
 
     val Ts = distinct_types (map snd all_comps);
     val arg_names = map fst args;
-    val valueN = Name.variant arg_names "'value";
-    val nameN = Name.variant (valueN::arg_names) "'name";
+    val valueN = singleton (Name.variant_list arg_names) "'value";
+    val nameN = singleton (Name.variant_list (valueN :: arg_names)) "'name";
     val valueT = TFree (valueN, Sign.defaultS thy);
     val nameT = TFree (nameN, Sign.defaultS thy);
     val stateT = nameT --> valueT;
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -849,7 +849,7 @@
       |>> (introduce_proxies format type_sys #> AAtom)
       ||> union (op =) atomic_types
     fun do_quant bs q s T t' =
-      let val s = Name.variant (map fst bs) s in
+      let val s = singleton (Name.variant_list (map fst bs)) s in
         do_formula ((s, T) :: bs) t'
         #>> mk_aquant q [(`make_bound_var s, SOME T)]
       end
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -281,7 +281,7 @@
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = take (length (hd descr)) recTs;
-    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
+    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
 
     fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
 
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -152,7 +152,7 @@
  
 fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
   let
-    val name = Name.variant used "a";
+    val name = singleton (Name.variant_list used) "a";
     fun expand constructors used ty ((_, []), _) =
           raise CASE_ERROR ("mk_case: expand_var_row", ~1)
       | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
@@ -264,11 +264,12 @@
 
         (* replace occurrences of dummy_pattern by distinct variables *)
         (* internalize constant names                                 *)
+        (* FIXME proper name context!? *)
         fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
               let val (t', used') = prep_pat t used
               in (c $ t' $ tT, used') end
           | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
-              let val x = Name.variant used "x"
+              let val x = singleton (Name.variant_list used) "x"
               in (Free (x, T), x :: used) end
           | prep_pat (Const (s, T)) used =
               (Const (intern_const_syntax s, T), used)
@@ -305,6 +306,7 @@
 
 (* destruct one level of pattern matching *)
 
+(* FIXME proper name context!? *)
 fun gen_dest_case name_of type_of tab d used t =
   (case apfst name_of (strip_comb t) of
     (SOME cname, ts as _ :: _) =>
@@ -345,7 +347,7 @@
                 val R = type_of t;
                 val dummy =
                   if d then Const (@{const_name dummy_pattern}, R)
-                  else Free (Name.variant used "x", R);
+                  else Free (singleton (Name.variant_list used) "x", R);
               in
                 SOME (x,
                   map mk_case
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -47,7 +47,7 @@
       |> Term.strip_comb
       |> apsnd (fst o split_last)
       |> list_comb;
-    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
+    val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
     val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
   in
     thms
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -263,7 +263,7 @@
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = take (length (hd descr)) recTs;
-    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
+    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -310,7 +310,7 @@
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = take (length (hd descr)) recTs;
-    val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
+    val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);
 
     fun make_split (((_, (_, _, constrs)), T), comb_t) =
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -75,7 +75,7 @@
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
       | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
         (*Universal quant: insert a free variable into body and continue*)
-        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
+        let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
         in dec_sko (subst_bound (Free(fname,T), p)) rhss end
       | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -205,7 +205,7 @@
       (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
         (Symbol.explode name)))
     val name'' = f (if name' = "" then empty else name')
-  in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
+  in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
 
 (** constant table **)
 
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Predicate_Compile/mode_inference.ML
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -249,7 +249,7 @@
           end
         else
           let
-            val s = Name.variant names "x"
+            val s = singleton (Name.variant_list names) "x"
             val v = Free (s, fastype_of t)
           in
             (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
@@ -257,7 +257,7 @@
 (*
   if is_constrt thy t then (t, (names, eqs)) else
     let
-      val s = Name.variant names "x"
+      val s = singleton (Name.variant_list names) "x"
       val v = Free (s, fastype_of t)
     in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
 *)
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -906,7 +906,7 @@
         val Type ("fun", [T, T']) = fastype_of comb;
         val (Const (case_name, _), fs) = strip_comb comb
         val used = Term.add_tfree_names comb []
-        val U = TFree (Name.variant used "'t", HOLogic.typeS)
+        val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
         val x = Free ("x", T)
         val f = Free ("f", T' --> U)
         fun apply_f f' =
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -302,7 +302,7 @@
   mk_random = (fn _ => error "no random generation"),
   additional_arguments = fn names =>
     let
-      val depth_name = Name.variant names "depth"
+      val depth_name = singleton (Name.variant_list names) "depth"
     in [Free (depth_name, @{typ code_numeral})] end,
   modify_funT = (fn T => let val (Ts, U) = strip_type T
   val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
@@ -563,7 +563,7 @@
       NONE => (Free (s, T), (names, (s, [])::vs))
     | SOME xs =>
         let
-          val s' = Name.variant names s;
+          val s' = singleton (Name.variant_list names) s;
           val v = Free (s', T)
         in
           (v, (s'::names, AList.update (op =) (s, v::xs) vs))
@@ -626,8 +626,8 @@
     val eqs'' =
       map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
     val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
-    val name = Name.variant names "x";
-    val name' = Name.variant (name :: names) "y";
+    val name = singleton (Name.variant_list names) "x";
+    val name' = singleton (Name.variant_list (name :: names)) "y";
     val T = HOLogic.mk_tupleT (map fastype_of out_ts);
     val U = fastype_of success_t;
     val U' = dest_predT compfuns U;
@@ -905,7 +905,7 @@
       let
         val (i, is) = argument_position_of mode position
         val inp_var = nth_pair is (nth in_ts' i)
-        val x = Name.variant all_vs "x"
+        val x = singleton (Name.variant_list all_vs) "x"
         val xt = Free (x, fastype_of inp_var)
         fun compile_single_case ((c, T), switched) =
           let
@@ -962,7 +962,7 @@
           (Free (hd param_vs, T), (tl param_vs, names))
         else
           let
-            val new = Name.variant names "x"
+            val new = singleton (Name.variant_list names) "x"
           in (Free (new, T), (param_vs, new :: names)) end)) inpTs
         (param_vs, (all_vs @ param_vs))
     val in_ts' = map_filter (map_filter_prod
@@ -1009,7 +1009,7 @@
 fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
     if eq_mode (m, Input) orelse eq_mode (m, Output) then
       let
-        val x = Name.variant names "x"
+        val x = singleton (Name.variant_list names) "x"
       in
         (Free (x, T), x :: names)
       end
@@ -1023,7 +1023,7 @@
   | mk_args is_eval ((m as Fun _), T) names =
     let
       val funT = funT_of PredicateCompFuns.compfuns m T
-      val x = Name.variant names "x"
+      val x = singleton (Name.variant_list names) "x"
       val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
       val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
       val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
@@ -1033,7 +1033,7 @@
     end
   | mk_args is_eval (_, T) names =
     let
-      val x = Name.variant names "x"
+      val x = singleton (Name.variant_list names) "x"
     in
       (Free (x, T), x :: names)
     end
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -118,7 +118,7 @@
           val absnames = Name.variant_list names (map fst vars)
           val frees = map2 (curry Free) absnames (map snd vars)
           val body' = subst_bounds (rev frees, body)
-          val resname = Name.variant (absnames @ names) "res"
+          val resname = singleton (Name.variant_list (absnames @ names)) "res"
           val resvar = Free (resname, fastype_of body)
           val t = flatten' body' ([], [])
             |> map (fn (res, (inner_names, inner_prems)) =>
@@ -241,7 +241,7 @@
                             HOLogic.mk_eq (@{term False}, Bound 0)))
                         end
                     val argvs' = map2 lift_arg Ts argvs
-                    val resname = Name.variant names' "res"
+                    val resname = singleton (Name.variant_list names') "res"
                     val resvar = Free (resname, body_type (fastype_of t))
                     val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
                   in (resvar, (resname :: names', prem :: prems')) end))
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -77,7 +77,7 @@
   if is_compound atom then
     let
       val atom = Envir.beta_norm (Pattern.eta_long [] atom)
-      val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+      val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
         ((Long_Name.base_name constname) ^ "_aux")
       val full_constname = Sign.full_bname thy constname
       val (params, args) = List.partition (is_predT o fastype_of)
@@ -108,7 +108,7 @@
       | SOME (atom', srs) =>
         let      
           val frees = map Free (Term.add_frees atom' [])
-          val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+          val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
            ((Long_Name.base_name constname) ^ "_aux")
           val full_constname = Sign.full_bname thy constname
           val constT = map fastype_of frees ---> HOLogic.boolT
@@ -239,8 +239,9 @@
             val vars = map Var (Term.add_vars abs_arg [])
             val abs_arg' = Logic.unvarify_global abs_arg
             val frees = map Free (Term.add_frees abs_arg' [])
-            val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
-              ((Long_Name.base_name constname) ^ "_hoaux")
+            val constname =
+              singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs))
+                ((Long_Name.base_name constname) ^ "_hoaux")
             val full_constname = Sign.full_bname thy constname
             val constT = map fastype_of frees ---> (fastype_of abs_arg')
             val const = Const (full_constname, constT)
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -73,7 +73,8 @@
     fun mk_fresh_name names =
       let
         val name =
-          Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
+          singleton (Name.variant_list names)
+            ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
         val bname = Sign.full_bname thy name
       in
         if Sign.declared_const thy bname then
@@ -119,7 +120,7 @@
     val add_vars = fold_aterms (fn Var v => cons v | _ => I);
     fun fresh_free T free_names =
       let
-        val free_name = Name.variant free_names "x"
+        val free_name = singleton (Name.variant_list free_names) "x"
       in
         (Free (free_name, T), free_name :: free_names)
       end
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -155,7 +155,7 @@
 fun close_form t =
   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   |> fold (fn ((s, i), T) => fn (t', taken) =>
-              let val s' = Name.variant taken s in
+              let val s' = singleton (Name.variant_list taken) s in
                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
                   else Term.all) T
                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -324,7 +324,7 @@
                               map_index (fn (i, t) => (t,(i,true))) R)
      val names = List.foldr OldTerm.add_term_names [] R
      val atype = type_of(hd pats)
-     and aname = Name.variant names "a"
+     and aname = singleton (Name.variant_list names) "a"
      val a = Free(aname,atype)
      val ty_info = Thry.match_info thy
      val ty_match = Thry.match_type thy
@@ -480,7 +480,7 @@
      val tych = Thry.typecheck thy
      val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
      val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
-     val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
+     val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
                    Rtype)
      val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
      val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
@@ -679,8 +679,8 @@
  in fn pats =>
  let val names = List.foldr OldTerm.add_term_names [] pats
      val T = type_of (hd pats)
-     val aname = Name.variant names "a"
-     val vname = Name.variant (aname::names) "v"
+     val aname = singleton (Name.variant_list names) "a"
+     val vname = singleton (Name.variant_list (aname::names)) "v"
      val a = Free (aname, T)
      val v = Free (vname, T)
      val a_eq_v = HOLogic.mk_eq(a,v)
@@ -830,8 +830,8 @@
     val (pats,TCsl) = ListPair.unzip pat_TCs_list
     val case_thm = complete_cases thy pats
     val domain = (type_of o hd) pats
-    val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
-                              [] (pats::TCsl)) "P"
+    val Pname = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
+                              [] (pats::TCsl))) "P"
     val P = Free(Pname, domain --> HOLogic.boolT)
     val Sinduct = Rules.SPEC (tych P) Sinduction
     val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
@@ -841,9 +841,10 @@
     val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
     val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
     val proved_cases = map (prove_case fconst thy) tasks
-    val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
-                    "v",
-                  domain)
+    val v =
+      Free (singleton
+        (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
+          domain)
     val vtyped = tych v
     val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
     val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -238,7 +238,7 @@
 
 fun dest_abs used (a as Abs(s, ty, M)) =
      let
-       val s' = Name.variant used s;
+       val s' = singleton (Name.variant_list used) s;
        val v = Free(s', ty);
      in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
      end
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -326,7 +326,7 @@
   (case AList.lookup (op =) vs s of
     NONE => (s, (names, (s, [s])::vs))
   | SOME xs =>
-      let val s' = Name.variant names s
+      let val s' = singleton (Name.variant_list names) s
       in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
 
 fun distinct_v (Var ((s, 0), T)) nvs =
@@ -414,7 +414,7 @@
     fun check_constrt t (names, eqs) =
       if is_constrt thy t then (t, (names, eqs))
       else
-        let val s = Name.variant names "x";
+        let val s = singleton (Name.variant_list names) "x";
         in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
 
     fun compile_eq (s, t) gr =
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -36,7 +36,7 @@
 
 fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
       let val (s', names') = (case names of
-          [] => (Name.variant used s, [])
+          [] => (singleton (Name.variant_list used) s, [])
         | name :: names' => (name, names'))
       in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
   | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
@@ -246,7 +246,7 @@
     handle Datatype_Aux.Datatype_Empty name' =>
       let
         val name = Long_Name.base_name name';
-        val dname = Name.variant used "Dummy";
+        val dname = singleton (Name.variant_list used) "Dummy";
       in
         thy
         |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
diff -r 28e71a685c84 -r 2b47822868e4 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/record.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -1662,7 +1662,7 @@
     val variants = map (fn Free (x, _) => x) vars_more;
     val ext = mk_ext vars_more;
     val s = Free (rN, extT);
-    val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
+    val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
 
     val inject_prop =
       let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
@@ -1677,7 +1677,7 @@
       (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
 
     val split_meta_prop =
-      let val P = Free (Name.variant variants "P", extT --> Term.propT) in
+      let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
         Logic.mk_equals
          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
       end;
@@ -1938,7 +1938,7 @@
     val all_vars = parent_vars @ vars;
     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
 
-    val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
+    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
     val moreT = TFree zeta;
     val more = Free (moreN, moreT);
     val full_moreN = full (Binding.name moreN);
@@ -2134,9 +2134,9 @@
 
     (* prepare propositions *)
     val _ = timing_msg "record preparing propositions";
-    val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
-    val C = Free (Name.variant all_variants "C", HOLogic.boolT);
-    val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
+    val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
+    val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
+    val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
 
     (*selectors*)
     val sel_conv_props =
@@ -2145,7 +2145,8 @@
     (*updates*)
     fun mk_upd_prop i (c, T) =
       let
-        val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
+        val x' =
+          Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
         val n = parent_fields_len + i;
         val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
       in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
@@ -2174,7 +2175,9 @@
 
     (*split*)
     val split_meta_prop =
-      let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
+      let
+        val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
+      in
         Logic.mk_equals
          (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
       end;
diff -r 28e71a685c84 -r 2b47822868e4 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -133,7 +133,7 @@
     val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
 
     (*obtain statements*)
-    val thesisN = Name.variant xs Auto_Bind.thesisN;
+    val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
     val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
 
     val that_name = if name = "" then thatN else name;
diff -r 28e71a685c84 -r 2b47822868e4 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/codegen.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -273,7 +273,7 @@
 
 fun preprocess_term thy t =
   let
-    val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
+    val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
     (* fake definition *)
     val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
     fun err () = error "preprocess_term: bad preprocessor"
diff -r 28e71a685c84 -r 2b47822868e4 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/drule.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -337,7 +337,7 @@
        [] => (fth, fn x => x)
      | vars =>
          let fun newName (Var(ix,_), (pairs,used)) =
-                   let val v = Name.variant used (string_of_indexname ix)
+                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
                    in  ((ix,v)::pairs, v::used)  end;
              val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
                (prop :: Thm.terms_of_tpairs tpairs, [])) vars
diff -r 28e71a685c84 -r 2b47822868e4 src/Pure/name.ML
--- a/src/Pure/name.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/name.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -26,7 +26,6 @@
   val invent_list: string list -> string -> int -> string list
   val variants: string list -> context -> string list * context
   val variant_list: string list -> string list -> string list
-  val variant: string list -> string -> string
   val desymbolize: bool -> string -> string
 end;
 
@@ -137,7 +136,6 @@
   in (x' ^ replicate_string n "_", ctxt') end);
 
 fun variant_list used names = #1 (make_context used |> variants names);
-fun variant used = singleton (variant_list used);
 
 
 (* names conforming to typical requirements of identifiers in the world outside *)
diff -r 28e71a685c84 -r 2b47822868e4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/proofterm.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -668,7 +668,7 @@
 local
 
 fun new_name (ix, (pairs,used)) =
-  let val v = Name.variant used (string_of_indexname ix)
+  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   in  ((ix, v) :: pairs, v :: used)  end;
 
 fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
diff -r 28e71a685c84 -r 2b47822868e4 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/term.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -936,7 +936,8 @@
       | name_clash (Abs (_, _, t)) = name_clash t
       | name_clash _ = false;
   in
-    if name_clash body then dest_abs (Name.variant [x] x, T, body)    (*potentially slow*)
+    if name_clash body then
+      dest_abs (singleton (Name.variant_list [x]) x, T, body)    (*potentially slow*)
     else (x, subst_bound (Free (x, T), body))
   end;
 
diff -r 28e71a685c84 -r 2b47822868e4 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/type.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -358,7 +358,7 @@
 local
 
 fun new_name (ix, (pairs, used)) =
-  let val v = Name.variant used (string_of_indexname ix)
+  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   in ((ix, v) :: pairs, v :: used) end;
 
 fun freeze_one alist (ix, sort) =
diff -r 28e71a685c84 -r 2b47822868e4 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -184,7 +184,7 @@
     fun fillup_param _ (_, SOME v) = v
       | fillup_param x (i, NONE) = x ^ string_of_int i;
     val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
-    val x = Name.variant (map_filter I fished1) "x";
+    val x = singleton (Name.variant_list (map_filter I fished1)) "x";
     val fished2 = map_index (fillup_param x) fished1;
     val (fished3, _) = Name.variants fished2 Name.context;
     val vars' = intro_vars fished3 vars;
diff -r 28e71a685c84 -r 2b47822868e4 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -416,7 +416,7 @@
   let
     val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
-    val v' = Name.variant (map fst vs) "a";
+    val v' = singleton (Name.variant_list (map fst vs)) "a";
     val vs' = (v', []) :: vs;
     val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
     val value_name = "Value.value.value"
diff -r 28e71a685c84 -r 2b47822868e4 src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/IsaPlanner/isand.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -190,7 +190,7 @@
       val tvars = List.foldr OldTerm.add_term_tvars [] ts;
       val (names',renamings) = 
           List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
-                         let val n2 = Name.variant Ns n in 
+                         let val n2 = singleton (Name.variant_list Ns) n in 
                            (n2::Ns, (tv, (n2,s))::Rs)
                          end) (tfree_names @ names,[]) tvars;
     in renamings end;
@@ -223,7 +223,7 @@
       val Ns = List.foldr OldTerm.add_term_names names ts;
       val (_,renamings) = 
           Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
-                    let val n2 = Name.variant Ns n in
+                    let val n2 = singleton (Name.variant_list Ns) n in
                       (n2 :: Ns, (v, (n2,ty)) :: Rs)
                     end) ((Ns,[]), vars);
     in renamings end;
diff -r 28e71a685c84 -r 2b47822868e4 src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -101,7 +101,7 @@
       val names = usednames_of_thm rule;
       val (fromnames,tonames,names2,Ts') = 
           Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
-                    let val n2 = Name.variant names n in
+                    let val n2 = singleton (Name.variant_list names) n in
                       (ctermify (Free(faken,ty)) :: rnf,
                        ctermify (Free(n2,ty)) :: rnt, 
                        n2 :: names,
@@ -146,7 +146,7 @@
       val vars_to_fix = union (op =) termvars cond_vs;
       val (renamings, names2) = 
           List.foldr (fn (((n,i),ty), (vs, names')) => 
-                    let val n' = Name.variant names' n in
+                    let val n' = singleton (Name.variant_list names') n in
                       ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
                     end)
                 ([], names) vars_to_fix;
@@ -154,7 +154,7 @@
 
 (* make a new fresh typefree instantiation for the given tvar *)
 fun new_tfree (tv as (ix,sort), (pairs,used)) =
-      let val v = Name.variant used (string_of_indexname ix)
+      let val v = singleton (Name.variant_list used) (string_of_indexname ix)
       in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
 
 
diff -r 28e71a685c84 -r 2b47822868e4 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/eqsubst.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -179,7 +179,7 @@
 fun fakefree_badbounds Ts t = 
     let val (FakeTs,Ts,newnames) = 
             List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
-                           let val newname = Name.variant usednames n
+                           let val newname = singleton (Name.variant_list usednames) n
                            in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
                                (newname,ty)::Ts, 
                                newname::usednames) end)
diff -r 28e71a685c84 -r 2b47822868e4 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -96,7 +96,7 @@
                Syntax.string_of_term ctxt t);
 
   (*** Construct the fixedpoint definition ***)
-  val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
+  val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
 
diff -r 28e71a685c84 -r 2b47822868e4 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -139,8 +139,9 @@
     (** make definition **)
 
     (*the recursive argument*)
-    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
-                        Ind_Syntax.iT)
+    val rec_arg =
+      Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
+        Ind_Syntax.iT)
 
     val def_tm = Logic.mk_equals
                     (subst_bound (rec_arg, fabs),