discontinued Name.variant to emphasize that this is old-style / indirect;
authorwenzelm
Thu Jun 09 16:34:49 2011 +0200 (2011-06-09)
changeset 433242b47822868e4
parent 43323 28e71a685c84
child 43325 4384f4ae0574
discontinued Name.variant to emphasize that this is old-style / indirect;
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Import/hol4rews.ML
src/HOL/Import/shuffler.ML
src/HOL/Inductive.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/List.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/mode_inference.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record.ML
src/Pure/Isar/obtain.ML
src/Pure/codegen.ML
src/Pure/drule.ML
src/Pure/name.ML
src/Pure/proofterm.ML
src/Pure/term.ML
src/Pure/type.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_target.ML
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/eqsubst.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -403,7 +403,7 @@
     1.4  
     1.5      (* calculate function arguments of case combinator *)
     1.6      val tns = map fst (Term.add_tfreesT lhsT [])
     1.7 -    val resultT = TFree (Name.variant tns "'t", @{sort pcpo})
     1.8 +    val resultT = TFree (singleton (Name.variant_list tns) "'t", @{sort pcpo})
     1.9      fun fTs T = map (fn (_, args) => map snd args -->> T) spec
    1.10      val fns = Datatype_Prop.indexify_names (map (K "f") spec)
    1.11      val fs = map Free (fns ~~ fTs resultT)
    1.12 @@ -768,7 +768,7 @@
    1.13      val resultT : typ =
    1.14        let
    1.15          val ts : string list = map fst (Term.add_tfreesT lhsT [])
    1.16 -        val t : string = Name.variant ts "'t"
    1.17 +        val t : string = singleton (Name.variant_list ts) "'t"
    1.18        in TFree (t, @{sort pcpo}) end
    1.19  
    1.20      (* define match combinators *)
     2.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 09 15:38:49 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Jun 09 16:34:49 2011 +0200
     2.3 @@ -234,7 +234,7 @@
     2.4            in comp_con T f rhs' (v::vs) taken' end
     2.5        | Const (c, cT) =>
     2.6            let
     2.7 -            val n = Name.variant taken "v"
     2.8 +            val n = singleton (Name.variant_list taken) "v"
     2.9              val v = Free(n, T)
    2.10              val m = Const(match_name c, matcherT (cT, fastype_of rhs))
    2.11              val k = big_lambdas vs rhs
     3.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Thu Jun 09 15:38:49 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Thu Jun 09 16:34:49 2011 +0200
     3.3 @@ -531,7 +531,7 @@
     3.4      (* prove strictness and reduction rules of pattern combinators *)
     3.5      local
     3.6        val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
     3.7 -      val rn = Name.variant tns "'r";
     3.8 +      val rn = singleton (Name.variant_list tns) "'r";
     3.9        val R = TFree (rn, @{sort pcpo});
    3.10        fun pat_lhs (pat, args) =
    3.11          let
     4.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jun 09 15:38:49 2011 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jun 09 16:34:49 2011 +0200
     4.3 @@ -618,7 +618,6 @@
     4.4  open Code_Thingol;
     4.5  
     4.6  fun imp_program naming =
     4.7 -
     4.8    let
     4.9      fun is_const c = case lookup_const naming c
    4.10       of SOME c' => (fn c'' => c' = c'')
    4.11 @@ -635,7 +634,7 @@
    4.12        | dest_abs (t, ty) =
    4.13            let
    4.14              val vs = fold_varnames cons t [];
    4.15 -            val v = Name.variant vs "x";
    4.16 +            val v = singleton (Name.variant_list vs) "x";
    4.17              val ty' = (hd o fst o unfold_fun) ty;
    4.18            in ((SOME v, ty'), t `$ IVar (SOME v)) end;
    4.19      fun force (t as IConst (c, _) `$ t') = if is_return c
     5.1 --- a/src/HOL/Import/hol4rews.ML	Thu Jun 09 15:38:49 2011 +0200
     5.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Jun 09 16:34:49 2011 +0200
     5.3 @@ -605,7 +605,7 @@
     5.4                  then F defname                 (* name_def *)
     5.5                  else if not (member (op =) used pdefname)
     5.6                  then F pdefname                (* name_primdef *)
     5.7 -                else F (Name.variant used pdefname) (* last resort *)
     5.8 +                else F (singleton (Name.variant_list used) pdefname) (* last resort *)
     5.9              end
    5.10      end
    5.11  
     6.1 --- a/src/HOL/Import/shuffler.ML	Thu Jun 09 15:38:49 2011 +0200
     6.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jun 09 16:34:49 2011 +0200
     6.3 @@ -228,7 +228,7 @@
     6.4          val (type_inst,_) =
     6.5              fold (fn (w as (v,_), S) => fn (inst, used) =>
     6.6                        let
     6.7 -                          val v' = Name.variant used v
     6.8 +                          val v' = singleton (Name.variant_list used) v
     6.9                        in
    6.10                            ((w,TFree(v',S))::inst,v'::used)
    6.11                        end)
    6.12 @@ -298,7 +298,7 @@
    6.13                then
    6.14                    let
    6.15                        val cert = cterm_of thy
    6.16 -                      val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
    6.17 +                      val v = Free (singleton (Name.variant_list (Term.add_free_names t [])) "v", xT)
    6.18                        val cv = cert v
    6.19                        val ct = cert t
    6.20                        val th = (Thm.assume ct)
    6.21 @@ -361,7 +361,7 @@
    6.22                        Type("fun",[aT,bT]) =>
    6.23                        let
    6.24                            val cert = cterm_of thy
    6.25 -                          val vname = Name.variant (Term.add_free_names t []) "v"
    6.26 +                          val vname = singleton (Name.variant_list (Term.add_free_names t [])) "v"
    6.27                            val v = Free(vname,aT)
    6.28                            val cv = cert v
    6.29                            val ct = cert t
     7.1 --- a/src/HOL/Inductive.thy	Thu Jun 09 15:38:49 2011 +0200
     7.2 +++ b/src/HOL/Inductive.thy	Thu Jun 09 16:34:49 2011 +0200
     7.3 @@ -295,7 +295,8 @@
     7.4  let
     7.5    fun fun_tr ctxt [cs] =
     7.6      let
     7.7 -      val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
     7.8 +      (* FIXME proper name context!? *)
     7.9 +      val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
    7.10        val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
    7.11      in lambda x ft end
    7.12  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
     8.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jun 09 15:38:49 2011 +0200
     8.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jun 09 16:34:49 2011 +0200
     8.3 @@ -113,8 +113,8 @@
     8.4  
     8.5  fun remove_suc thy thms =
     8.6    let
     8.7 -    val vname = Name.variant (map fst
     8.8 -      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
     8.9 +    val vname = singleton (Name.variant_list (map fst
    8.10 +      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
    8.11      val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
    8.12      fun lhs_of th = snd (Thm.dest_comb
    8.13        (fst (Thm.dest_comb (cprop_of th))));
    8.14 @@ -166,8 +166,8 @@
    8.15  
    8.16  fun remove_suc_clause thy thms =
    8.17    let
    8.18 -    val vname = Name.variant (map fst
    8.19 -      (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
    8.20 +    val vname = singleton (Name.variant_list (map fst
    8.21 +      (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "x";
    8.22      fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
    8.23        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
    8.24        | find_var _ = NONE;
     9.1 --- a/src/HOL/List.thy	Thu Jun 09 15:38:49 2011 +0200
     9.2 +++ b/src/HOL/List.thy	Thu Jun 09 16:34:49 2011 +0200
     9.3 @@ -383,7 +383,8 @@
     9.4  
     9.5    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
     9.6      let
     9.7 -      val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
     9.8 +      (* FIXME proper name context!? *)
     9.9 +      val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
    9.10        val e = if opti then singl e else e;
    9.11        val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
    9.12        val case2 =
    10.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 09 15:38:49 2011 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 09 16:34:49 2011 +0200
    10.3 @@ -622,7 +622,7 @@
    10.4                (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
    10.5          let
    10.6            val permT = mk_permT
    10.7 -            (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
    10.8 +            (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
    10.9            val pi = Free ("pi", permT);
   10.10            val T = Type (Sign.intern_type thy name, map TFree tvs);
   10.11          in apfst (pair r o hd)
   10.12 @@ -1169,7 +1169,7 @@
   10.13          val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
   10.14          val frees = tnames ~~ Ts;
   10.15          val frees' = partition_cargs idxs frees;
   10.16 -        val z = (Name.variant tnames "z", fsT);
   10.17 +        val z = (singleton (Name.variant_list tnames) "z", fsT);
   10.18  
   10.19          fun mk_prem ((dt, s), T) =
   10.20            let
    11.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 15:38:49 2011 +0200
    11.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 16:34:49 2011 +0200
    11.3 @@ -207,7 +207,7 @@
    11.4  fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) =
    11.5    let
    11.6      val used = map fst (fold Term.add_frees fs []);
    11.7 -    val x = (Name.variant used "x", dummyT);
    11.8 +    val x = (singleton (Name.variant_list used) "x", dummyT);
    11.9      val frees = ls @ x :: rs;
   11.10      val raw_rhs = list_abs_free (frees,
   11.11        list_comb (Const (rec_name, dummyT), fs @ [Free x]))
    12.1 --- a/src/HOL/Statespace/state_space.ML	Thu Jun 09 15:38:49 2011 +0200
    12.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Jun 09 16:34:49 2011 +0200
    12.3 @@ -379,8 +379,8 @@
    12.4  
    12.5      val Ts = distinct_types (map snd all_comps);
    12.6      val arg_names = map fst args;
    12.7 -    val valueN = Name.variant arg_names "'value";
    12.8 -    val nameN = Name.variant (valueN::arg_names) "'name";
    12.9 +    val valueN = singleton (Name.variant_list arg_names) "'value";
   12.10 +    val nameN = singleton (Name.variant_list (valueN :: arg_names)) "'name";
   12.11      val valueT = TFree (valueN, Sign.defaultS thy);
   12.12      val nameT = TFree (nameN, Sign.defaultS thy);
   12.13      val stateT = nameT --> valueT;
    13.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 15:38:49 2011 +0200
    13.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 16:34:49 2011 +0200
    13.3 @@ -849,7 +849,7 @@
    13.4        |>> (introduce_proxies format type_sys #> AAtom)
    13.5        ||> union (op =) atomic_types
    13.6      fun do_quant bs q s T t' =
    13.7 -      let val s = Name.variant (map fst bs) s in
    13.8 +      let val s = singleton (Name.variant_list (map fst bs)) s in
    13.9          do_formula ((s, T) :: bs) t'
   13.10          #>> mk_aquant q [(`make_bound_var s, SOME T)]
   13.11        end
    14.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jun 09 15:38:49 2011 +0200
    14.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Jun 09 16:34:49 2011 +0200
    14.3 @@ -281,7 +281,7 @@
    14.4      val recTs = Datatype_Aux.get_rec_types descr' sorts;
    14.5      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    14.6      val newTs = take (length (hd descr)) recTs;
    14.7 -    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
    14.8 +    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
    14.9  
   14.10      fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
   14.11  
    15.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jun 09 15:38:49 2011 +0200
    15.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jun 09 16:34:49 2011 +0200
    15.3 @@ -152,7 +152,7 @@
    15.4   
    15.5  fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
    15.6    let
    15.7 -    val name = Name.variant used "a";
    15.8 +    val name = singleton (Name.variant_list used) "a";
    15.9      fun expand constructors used ty ((_, []), _) =
   15.10            raise CASE_ERROR ("mk_case: expand_var_row", ~1)
   15.11        | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
   15.12 @@ -264,11 +264,12 @@
   15.13  
   15.14          (* replace occurrences of dummy_pattern by distinct variables *)
   15.15          (* internalize constant names                                 *)
   15.16 +        (* FIXME proper name context!? *)
   15.17          fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
   15.18                let val (t', used') = prep_pat t used
   15.19                in (c $ t' $ tT, used') end
   15.20            | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
   15.21 -              let val x = Name.variant used "x"
   15.22 +              let val x = singleton (Name.variant_list used) "x"
   15.23                in (Free (x, T), x :: used) end
   15.24            | prep_pat (Const (s, T)) used =
   15.25                (Const (intern_const_syntax s, T), used)
   15.26 @@ -305,6 +306,7 @@
   15.27  
   15.28  (* destruct one level of pattern matching *)
   15.29  
   15.30 +(* FIXME proper name context!? *)
   15.31  fun gen_dest_case name_of type_of tab d used t =
   15.32    (case apfst name_of (strip_comb t) of
   15.33      (SOME cname, ts as _ :: _) =>
   15.34 @@ -345,7 +347,7 @@
   15.35                  val R = type_of t;
   15.36                  val dummy =
   15.37                    if d then Const (@{const_name dummy_pattern}, R)
   15.38 -                  else Free (Name.variant used "x", R);
   15.39 +                  else Free (singleton (Name.variant_list used) "x", R);
   15.40                in
   15.41                  SOME (x,
   15.42                    map mk_case
    16.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Jun 09 15:38:49 2011 +0200
    16.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Jun 09 16:34:49 2011 +0200
    16.3 @@ -47,7 +47,7 @@
    16.4        |> Term.strip_comb
    16.5        |> apsnd (fst o split_last)
    16.6        |> list_comb;
    16.7 -    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
    16.8 +    val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
    16.9      val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
   16.10    in
   16.11      thms
    17.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Jun 09 15:38:49 2011 +0200
    17.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Jun 09 16:34:49 2011 +0200
    17.3 @@ -263,7 +263,7 @@
    17.4      val recTs = Datatype_Aux.get_rec_types descr' sorts;
    17.5      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    17.6      val newTs = take (length (hd descr)) recTs;
    17.7 -    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
    17.8 +    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
    17.9  
   17.10      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   17.11        map (fn (_, cargs) =>
   17.12 @@ -310,7 +310,7 @@
   17.13      val recTs = Datatype_Aux.get_rec_types descr' sorts;
   17.14      val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   17.15      val newTs = take (length (hd descr)) recTs;
   17.16 -    val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
   17.17 +    val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
   17.18      val P = Free ("P", T' --> HOLogic.boolT);
   17.19  
   17.20      fun make_split (((_, (_, _, constrs)), T), comb_t) =
    18.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jun 09 15:38:49 2011 +0200
    18.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Jun 09 16:34:49 2011 +0200
    18.3 @@ -75,7 +75,7 @@
    18.4          in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    18.5        | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
    18.6          (*Universal quant: insert a free variable into body and continue*)
    18.7 -        let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    18.8 +        let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
    18.9          in dec_sko (subst_bound (Free(fname,T), p)) rhss end
   18.10        | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
   18.11        | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    19.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jun 09 15:38:49 2011 +0200
    19.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jun 09 16:34:49 2011 +0200
    19.3 @@ -205,7 +205,7 @@
    19.4        (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
    19.5          (Symbol.explode name)))
    19.6      val name'' = f (if name' = "" then empty else name')
    19.7 -  in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
    19.8 +  in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
    19.9  
   19.10  (** constant table **)
   19.11  
    20.1 --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Jun 09 15:38:49 2011 +0200
    20.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Thu Jun 09 16:34:49 2011 +0200
    20.3 @@ -249,7 +249,7 @@
    20.4            end
    20.5          else
    20.6            let
    20.7 -            val s = Name.variant names "x"
    20.8 +            val s = singleton (Name.variant_list names) "x"
    20.9              val v = Free (s, fastype_of t)
   20.10            in
   20.11              (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
   20.12 @@ -257,7 +257,7 @@
   20.13  (*
   20.14    if is_constrt thy t then (t, (names, eqs)) else
   20.15      let
   20.16 -      val s = Name.variant names "x"
   20.17 +      val s = singleton (Name.variant_list names) "x"
   20.18        val v = Free (s, fastype_of t)
   20.19      in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
   20.20  *)
    21.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 15:38:49 2011 +0200
    21.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 16:34:49 2011 +0200
    21.3 @@ -906,7 +906,7 @@
    21.4          val Type ("fun", [T, T']) = fastype_of comb;
    21.5          val (Const (case_name, _), fs) = strip_comb comb
    21.6          val used = Term.add_tfree_names comb []
    21.7 -        val U = TFree (Name.variant used "'t", HOLogic.typeS)
    21.8 +        val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
    21.9          val x = Free ("x", T)
   21.10          val f = Free ("f", T' --> U)
   21.11          fun apply_f f' =
    22.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 09 15:38:49 2011 +0200
    22.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 09 16:34:49 2011 +0200
    22.3 @@ -302,7 +302,7 @@
    22.4    mk_random = (fn _ => error "no random generation"),
    22.5    additional_arguments = fn names =>
    22.6      let
    22.7 -      val depth_name = Name.variant names "depth"
    22.8 +      val depth_name = singleton (Name.variant_list names) "depth"
    22.9      in [Free (depth_name, @{typ code_numeral})] end,
   22.10    modify_funT = (fn T => let val (Ts, U) = strip_type T
   22.11    val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
   22.12 @@ -563,7 +563,7 @@
   22.13        NONE => (Free (s, T), (names, (s, [])::vs))
   22.14      | SOME xs =>
   22.15          let
   22.16 -          val s' = Name.variant names s;
   22.17 +          val s' = singleton (Name.variant_list names) s;
   22.18            val v = Free (s', T)
   22.19          in
   22.20            (v, (s'::names, AList.update (op =) (s, v::xs) vs))
   22.21 @@ -626,8 +626,8 @@
   22.22      val eqs'' =
   22.23        map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
   22.24      val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
   22.25 -    val name = Name.variant names "x";
   22.26 -    val name' = Name.variant (name :: names) "y";
   22.27 +    val name = singleton (Name.variant_list names) "x";
   22.28 +    val name' = singleton (Name.variant_list (name :: names)) "y";
   22.29      val T = HOLogic.mk_tupleT (map fastype_of out_ts);
   22.30      val U = fastype_of success_t;
   22.31      val U' = dest_predT compfuns U;
   22.32 @@ -905,7 +905,7 @@
   22.33        let
   22.34          val (i, is) = argument_position_of mode position
   22.35          val inp_var = nth_pair is (nth in_ts' i)
   22.36 -        val x = Name.variant all_vs "x"
   22.37 +        val x = singleton (Name.variant_list all_vs) "x"
   22.38          val xt = Free (x, fastype_of inp_var)
   22.39          fun compile_single_case ((c, T), switched) =
   22.40            let
   22.41 @@ -962,7 +962,7 @@
   22.42            (Free (hd param_vs, T), (tl param_vs, names))
   22.43          else
   22.44            let
   22.45 -            val new = Name.variant names "x"
   22.46 +            val new = singleton (Name.variant_list names) "x"
   22.47            in (Free (new, T), (param_vs, new :: names)) end)) inpTs
   22.48          (param_vs, (all_vs @ param_vs))
   22.49      val in_ts' = map_filter (map_filter_prod
   22.50 @@ -1009,7 +1009,7 @@
   22.51  fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
   22.52      if eq_mode (m, Input) orelse eq_mode (m, Output) then
   22.53        let
   22.54 -        val x = Name.variant names "x"
   22.55 +        val x = singleton (Name.variant_list names) "x"
   22.56        in
   22.57          (Free (x, T), x :: names)
   22.58        end
   22.59 @@ -1023,7 +1023,7 @@
   22.60    | mk_args is_eval ((m as Fun _), T) names =
   22.61      let
   22.62        val funT = funT_of PredicateCompFuns.compfuns m T
   22.63 -      val x = Name.variant names "x"
   22.64 +      val x = singleton (Name.variant_list names) "x"
   22.65        val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
   22.66        val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
   22.67        val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
   22.68 @@ -1033,7 +1033,7 @@
   22.69      end
   22.70    | mk_args is_eval (_, T) names =
   22.71      let
   22.72 -      val x = Name.variant names "x"
   22.73 +      val x = singleton (Name.variant_list names) "x"
   22.74      in
   22.75        (Free (x, T), x :: names)
   22.76      end
    23.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 15:38:49 2011 +0200
    23.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 16:34:49 2011 +0200
    23.3 @@ -118,7 +118,7 @@
    23.4            val absnames = Name.variant_list names (map fst vars)
    23.5            val frees = map2 (curry Free) absnames (map snd vars)
    23.6            val body' = subst_bounds (rev frees, body)
    23.7 -          val resname = Name.variant (absnames @ names) "res"
    23.8 +          val resname = singleton (Name.variant_list (absnames @ names)) "res"
    23.9            val resvar = Free (resname, fastype_of body)
   23.10            val t = flatten' body' ([], [])
   23.11              |> map (fn (res, (inner_names, inner_prems)) =>
   23.12 @@ -241,7 +241,7 @@
   23.13                              HOLogic.mk_eq (@{term False}, Bound 0)))
   23.14                          end
   23.15                      val argvs' = map2 lift_arg Ts argvs
   23.16 -                    val resname = Name.variant names' "res"
   23.17 +                    val resname = singleton (Name.variant_list names') "res"
   23.18                      val resvar = Free (resname, body_type (fastype_of t))
   23.19                      val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
   23.20                    in (resvar, (resname :: names', prem :: prems')) end))
    24.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Jun 09 15:38:49 2011 +0200
    24.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Jun 09 16:34:49 2011 +0200
    24.3 @@ -77,7 +77,7 @@
    24.4    if is_compound atom then
    24.5      let
    24.6        val atom = Envir.beta_norm (Pattern.eta_long [] atom)
    24.7 -      val constname = Name.variant (map (Long_Name.base_name o fst) defs)
    24.8 +      val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
    24.9          ((Long_Name.base_name constname) ^ "_aux")
   24.10        val full_constname = Sign.full_bname thy constname
   24.11        val (params, args) = List.partition (is_predT o fastype_of)
   24.12 @@ -108,7 +108,7 @@
   24.13        | SOME (atom', srs) =>
   24.14          let      
   24.15            val frees = map Free (Term.add_frees atom' [])
   24.16 -          val constname = Name.variant (map (Long_Name.base_name o fst) defs)
   24.17 +          val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
   24.18             ((Long_Name.base_name constname) ^ "_aux")
   24.19            val full_constname = Sign.full_bname thy constname
   24.20            val constT = map fastype_of frees ---> HOLogic.boolT
   24.21 @@ -239,8 +239,9 @@
   24.22              val vars = map Var (Term.add_vars abs_arg [])
   24.23              val abs_arg' = Logic.unvarify_global abs_arg
   24.24              val frees = map Free (Term.add_frees abs_arg' [])
   24.25 -            val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
   24.26 -              ((Long_Name.base_name constname) ^ "_hoaux")
   24.27 +            val constname =
   24.28 +              singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs))
   24.29 +                ((Long_Name.base_name constname) ^ "_hoaux")
   24.30              val full_constname = Sign.full_bname thy constname
   24.31              val constT = map fastype_of frees ---> (fastype_of abs_arg')
   24.32              val const = Const (full_constname, constT)
    25.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Jun 09 15:38:49 2011 +0200
    25.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Jun 09 16:34:49 2011 +0200
    25.3 @@ -73,7 +73,8 @@
    25.4      fun mk_fresh_name names =
    25.5        let
    25.6          val name =
    25.7 -          Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
    25.8 +          singleton (Name.variant_list names)
    25.9 +            ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
   25.10          val bname = Sign.full_bname thy name
   25.11        in
   25.12          if Sign.declared_const thy bname then
   25.13 @@ -119,7 +120,7 @@
   25.14      val add_vars = fold_aterms (fn Var v => cons v | _ => I);
   25.15      fun fresh_free T free_names =
   25.16        let
   25.17 -        val free_name = Name.variant free_names "x"
   25.18 +        val free_name = singleton (Name.variant_list free_names) "x"
   25.19        in
   25.20          (Free (free_name, T), free_name :: free_names)
   25.21        end
    26.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 09 15:38:49 2011 +0200
    26.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 09 16:34:49 2011 +0200
    26.3 @@ -155,7 +155,7 @@
    26.4  fun close_form t =
    26.5    (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
    26.6    |> fold (fn ((s, i), T) => fn (t', taken) =>
    26.7 -              let val s' = Name.variant taken s in
    26.8 +              let val s' = singleton (Name.variant_list taken) s in
    26.9                  ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   26.10                    else Term.all) T
   26.11                   $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
    27.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Jun 09 15:38:49 2011 +0200
    27.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Jun 09 16:34:49 2011 +0200
    27.3 @@ -324,7 +324,7 @@
    27.4                                map_index (fn (i, t) => (t,(i,true))) R)
    27.5       val names = List.foldr OldTerm.add_term_names [] R
    27.6       val atype = type_of(hd pats)
    27.7 -     and aname = Name.variant names "a"
    27.8 +     and aname = singleton (Name.variant_list names) "a"
    27.9       val a = Free(aname,atype)
   27.10       val ty_info = Thry.match_info thy
   27.11       val ty_match = Thry.match_type thy
   27.12 @@ -480,7 +480,7 @@
   27.13       val tych = Thry.typecheck thy
   27.14       val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
   27.15       val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   27.16 -     val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
   27.17 +     val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
   27.18                     Rtype)
   27.19       val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
   27.20       val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
   27.21 @@ -679,8 +679,8 @@
   27.22   in fn pats =>
   27.23   let val names = List.foldr OldTerm.add_term_names [] pats
   27.24       val T = type_of (hd pats)
   27.25 -     val aname = Name.variant names "a"
   27.26 -     val vname = Name.variant (aname::names) "v"
   27.27 +     val aname = singleton (Name.variant_list names) "a"
   27.28 +     val vname = singleton (Name.variant_list (aname::names)) "v"
   27.29       val a = Free (aname, T)
   27.30       val v = Free (vname, T)
   27.31       val a_eq_v = HOLogic.mk_eq(a,v)
   27.32 @@ -830,8 +830,8 @@
   27.33      val (pats,TCsl) = ListPair.unzip pat_TCs_list
   27.34      val case_thm = complete_cases thy pats
   27.35      val domain = (type_of o hd) pats
   27.36 -    val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
   27.37 -                              [] (pats::TCsl)) "P"
   27.38 +    val Pname = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
   27.39 +                              [] (pats::TCsl))) "P"
   27.40      val P = Free(Pname, domain --> HOLogic.boolT)
   27.41      val Sinduct = Rules.SPEC (tych P) Sinduction
   27.42      val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
   27.43 @@ -841,9 +841,10 @@
   27.44      val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
   27.45      val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
   27.46      val proved_cases = map (prove_case fconst thy) tasks
   27.47 -    val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
   27.48 -                    "v",
   27.49 -                  domain)
   27.50 +    val v =
   27.51 +      Free (singleton
   27.52 +        (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
   27.53 +          domain)
   27.54      val vtyped = tych v
   27.55      val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   27.56      val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
    28.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Thu Jun 09 15:38:49 2011 +0200
    28.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Jun 09 16:34:49 2011 +0200
    28.3 @@ -238,7 +238,7 @@
    28.4  
    28.5  fun dest_abs used (a as Abs(s, ty, M)) =
    28.6       let
    28.7 -       val s' = Name.variant used s;
    28.8 +       val s' = singleton (Name.variant_list used) s;
    28.9         val v = Free(s', ty);
   28.10       in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
   28.11       end
    29.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jun 09 15:38:49 2011 +0200
    29.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jun 09 16:34:49 2011 +0200
    29.3 @@ -326,7 +326,7 @@
    29.4    (case AList.lookup (op =) vs s of
    29.5      NONE => (s, (names, (s, [s])::vs))
    29.6    | SOME xs =>
    29.7 -      let val s' = Name.variant names s
    29.8 +      let val s' = singleton (Name.variant_list names) s
    29.9        in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
   29.10  
   29.11  fun distinct_v (Var ((s, 0), T)) nvs =
   29.12 @@ -414,7 +414,7 @@
   29.13      fun check_constrt t (names, eqs) =
   29.14        if is_constrt thy t then (t, (names, eqs))
   29.15        else
   29.16 -        let val s = Name.variant names "x";
   29.17 +        let val s = singleton (Name.variant_list names) "x";
   29.18          in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
   29.19  
   29.20      fun compile_eq (s, t) gr =
    30.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jun 09 15:38:49 2011 +0200
    30.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jun 09 16:34:49 2011 +0200
    30.3 @@ -36,7 +36,7 @@
    30.4  
    30.5  fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
    30.6        let val (s', names') = (case names of
    30.7 -          [] => (Name.variant used s, [])
    30.8 +          [] => (singleton (Name.variant_list used) s, [])
    30.9          | name :: names' => (name, names'))
   30.10        in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
   30.11    | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
   30.12 @@ -246,7 +246,7 @@
   30.13      handle Datatype_Aux.Datatype_Empty name' =>
   30.14        let
   30.15          val name = Long_Name.base_name name';
   30.16 -        val dname = Name.variant used "Dummy";
   30.17 +        val dname = singleton (Name.variant_list used) "Dummy";
   30.18        in
   30.19          thy
   30.20          |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
    31.1 --- a/src/HOL/Tools/record.ML	Thu Jun 09 15:38:49 2011 +0200
    31.2 +++ b/src/HOL/Tools/record.ML	Thu Jun 09 16:34:49 2011 +0200
    31.3 @@ -1662,7 +1662,7 @@
    31.4      val variants = map (fn Free (x, _) => x) vars_more;
    31.5      val ext = mk_ext vars_more;
    31.6      val s = Free (rN, extT);
    31.7 -    val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
    31.8 +    val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
    31.9  
   31.10      val inject_prop =
   31.11        let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
   31.12 @@ -1677,7 +1677,7 @@
   31.13        (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
   31.14  
   31.15      val split_meta_prop =
   31.16 -      let val P = Free (Name.variant variants "P", extT --> Term.propT) in
   31.17 +      let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
   31.18          Logic.mk_equals
   31.19           (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
   31.20        end;
   31.21 @@ -1938,7 +1938,7 @@
   31.22      val all_vars = parent_vars @ vars;
   31.23      val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
   31.24  
   31.25 -    val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
   31.26 +    val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
   31.27      val moreT = TFree zeta;
   31.28      val more = Free (moreN, moreT);
   31.29      val full_moreN = full (Binding.name moreN);
   31.30 @@ -2134,9 +2134,9 @@
   31.31  
   31.32      (* prepare propositions *)
   31.33      val _ = timing_msg "record preparing propositions";
   31.34 -    val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
   31.35 -    val C = Free (Name.variant all_variants "C", HOLogic.boolT);
   31.36 -    val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
   31.37 +    val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
   31.38 +    val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
   31.39 +    val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
   31.40  
   31.41      (*selectors*)
   31.42      val sel_conv_props =
   31.43 @@ -2145,7 +2145,8 @@
   31.44      (*updates*)
   31.45      fun mk_upd_prop i (c, T) =
   31.46        let
   31.47 -        val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
   31.48 +        val x' =
   31.49 +          Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
   31.50          val n = parent_fields_len + i;
   31.51          val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
   31.52        in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
   31.53 @@ -2174,7 +2175,9 @@
   31.54  
   31.55      (*split*)
   31.56      val split_meta_prop =
   31.57 -      let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
   31.58 +      let
   31.59 +        val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
   31.60 +      in
   31.61          Logic.mk_equals
   31.62           (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
   31.63        end;
    32.1 --- a/src/Pure/Isar/obtain.ML	Thu Jun 09 15:38:49 2011 +0200
    32.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jun 09 16:34:49 2011 +0200
    32.3 @@ -133,7 +133,7 @@
    32.4      val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
    32.5  
    32.6      (*obtain statements*)
    32.7 -    val thesisN = Name.variant xs Auto_Bind.thesisN;
    32.8 +    val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
    32.9      val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
   32.10  
   32.11      val that_name = if name = "" then thatN else name;
    33.1 --- a/src/Pure/codegen.ML	Thu Jun 09 15:38:49 2011 +0200
    33.2 +++ b/src/Pure/codegen.ML	Thu Jun 09 16:34:49 2011 +0200
    33.3 @@ -273,7 +273,7 @@
    33.4  
    33.5  fun preprocess_term thy t =
    33.6    let
    33.7 -    val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
    33.8 +    val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
    33.9      (* fake definition *)
   33.10      val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
   33.11      fun err () = error "preprocess_term: bad preprocessor"
    34.1 --- a/src/Pure/drule.ML	Thu Jun 09 15:38:49 2011 +0200
    34.2 +++ b/src/Pure/drule.ML	Thu Jun 09 16:34:49 2011 +0200
    34.3 @@ -337,7 +337,7 @@
    34.4         [] => (fth, fn x => x)
    34.5       | vars =>
    34.6           let fun newName (Var(ix,_), (pairs,used)) =
    34.7 -                   let val v = Name.variant used (string_of_indexname ix)
    34.8 +                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
    34.9                     in  ((ix,v)::pairs, v::used)  end;
   34.10               val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
   34.11                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars
    35.1 --- a/src/Pure/name.ML	Thu Jun 09 15:38:49 2011 +0200
    35.2 +++ b/src/Pure/name.ML	Thu Jun 09 16:34:49 2011 +0200
    35.3 @@ -26,7 +26,6 @@
    35.4    val invent_list: string list -> string -> int -> string list
    35.5    val variants: string list -> context -> string list * context
    35.6    val variant_list: string list -> string list -> string list
    35.7 -  val variant: string list -> string -> string
    35.8    val desymbolize: bool -> string -> string
    35.9  end;
   35.10  
   35.11 @@ -137,7 +136,6 @@
   35.12    in (x' ^ replicate_string n "_", ctxt') end);
   35.13  
   35.14  fun variant_list used names = #1 (make_context used |> variants names);
   35.15 -fun variant used = singleton (variant_list used);
   35.16  
   35.17  
   35.18  (* names conforming to typical requirements of identifiers in the world outside *)
    36.1 --- a/src/Pure/proofterm.ML	Thu Jun 09 15:38:49 2011 +0200
    36.2 +++ b/src/Pure/proofterm.ML	Thu Jun 09 16:34:49 2011 +0200
    36.3 @@ -668,7 +668,7 @@
    36.4  local
    36.5  
    36.6  fun new_name (ix, (pairs,used)) =
    36.7 -  let val v = Name.variant used (string_of_indexname ix)
    36.8 +  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
    36.9    in  ((ix, v) :: pairs, v :: used)  end;
   36.10  
   36.11  fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
    37.1 --- a/src/Pure/term.ML	Thu Jun 09 15:38:49 2011 +0200
    37.2 +++ b/src/Pure/term.ML	Thu Jun 09 16:34:49 2011 +0200
    37.3 @@ -936,7 +936,8 @@
    37.4        | name_clash (Abs (_, _, t)) = name_clash t
    37.5        | name_clash _ = false;
    37.6    in
    37.7 -    if name_clash body then dest_abs (Name.variant [x] x, T, body)    (*potentially slow*)
    37.8 +    if name_clash body then
    37.9 +      dest_abs (singleton (Name.variant_list [x]) x, T, body)    (*potentially slow*)
   37.10      else (x, subst_bound (Free (x, T), body))
   37.11    end;
   37.12  
    38.1 --- a/src/Pure/type.ML	Thu Jun 09 15:38:49 2011 +0200
    38.2 +++ b/src/Pure/type.ML	Thu Jun 09 16:34:49 2011 +0200
    38.3 @@ -358,7 +358,7 @@
    38.4  local
    38.5  
    38.6  fun new_name (ix, (pairs, used)) =
    38.7 -  let val v = Name.variant used (string_of_indexname ix)
    38.8 +  let val v = singleton (Name.variant_list used) (string_of_indexname ix)
    38.9    in ((ix, v) :: pairs, v :: used) end;
   38.10  
   38.11  fun freeze_one alist (ix, sort) =
    39.1 --- a/src/Tools/Code/code_printer.ML	Thu Jun 09 15:38:49 2011 +0200
    39.2 +++ b/src/Tools/Code/code_printer.ML	Thu Jun 09 16:34:49 2011 +0200
    39.3 @@ -184,7 +184,7 @@
    39.4      fun fillup_param _ (_, SOME v) = v
    39.5        | fillup_param x (i, NONE) = x ^ string_of_int i;
    39.6      val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
    39.7 -    val x = Name.variant (map_filter I fished1) "x";
    39.8 +    val x = singleton (Name.variant_list (map_filter I fished1)) "x";
    39.9      val fished2 = map_index (fillup_param x) fished1;
   39.10      val (fished3, _) = Name.variants fished2 Name.context;
   39.11      val vars' = intro_vars fished3 vars;
    40.1 --- a/src/Tools/Code/code_target.ML	Thu Jun 09 15:38:49 2011 +0200
    40.2 +++ b/src/Tools/Code/code_target.ML	Thu Jun 09 16:34:49 2011 +0200
    40.3 @@ -416,7 +416,7 @@
    40.4    let
    40.5      val _ = if Code_Thingol.contains_dict_var t then
    40.6        error "Term to be evaluated contains free dictionaries" else ();
    40.7 -    val v' = Name.variant (map fst vs) "a";
    40.8 +    val v' = singleton (Name.variant_list (map fst vs)) "a";
    40.9      val vs' = (v', []) :: vs;
   40.10      val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
   40.11      val value_name = "Value.value.value"
    41.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu Jun 09 15:38:49 2011 +0200
    41.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu Jun 09 16:34:49 2011 +0200
    41.3 @@ -190,7 +190,7 @@
    41.4        val tvars = List.foldr OldTerm.add_term_tvars [] ts;
    41.5        val (names',renamings) = 
    41.6            List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
    41.7 -                         let val n2 = Name.variant Ns n in 
    41.8 +                         let val n2 = singleton (Name.variant_list Ns) n in 
    41.9                             (n2::Ns, (tv, (n2,s))::Rs)
   41.10                           end) (tfree_names @ names,[]) tvars;
   41.11      in renamings end;
   41.12 @@ -223,7 +223,7 @@
   41.13        val Ns = List.foldr OldTerm.add_term_names names ts;
   41.14        val (_,renamings) = 
   41.15            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   41.16 -                    let val n2 = Name.variant Ns n in
   41.17 +                    let val n2 = singleton (Name.variant_list Ns) n in
   41.18                        (n2 :: Ns, (v, (n2,ty)) :: Rs)
   41.19                      end) ((Ns,[]), vars);
   41.20      in renamings end;
    42.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu Jun 09 15:38:49 2011 +0200
    42.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu Jun 09 16:34:49 2011 +0200
    42.3 @@ -101,7 +101,7 @@
    42.4        val names = usednames_of_thm rule;
    42.5        val (fromnames,tonames,names2,Ts') = 
    42.6            Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
    42.7 -                    let val n2 = Name.variant names n in
    42.8 +                    let val n2 = singleton (Name.variant_list names) n in
    42.9                        (ctermify (Free(faken,ty)) :: rnf,
   42.10                         ctermify (Free(n2,ty)) :: rnt, 
   42.11                         n2 :: names,
   42.12 @@ -146,7 +146,7 @@
   42.13        val vars_to_fix = union (op =) termvars cond_vs;
   42.14        val (renamings, names2) = 
   42.15            List.foldr (fn (((n,i),ty), (vs, names')) => 
   42.16 -                    let val n' = Name.variant names' n in
   42.17 +                    let val n' = singleton (Name.variant_list names') n in
   42.18                        ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   42.19                      end)
   42.20                  ([], names) vars_to_fix;
   42.21 @@ -154,7 +154,7 @@
   42.22  
   42.23  (* make a new fresh typefree instantiation for the given tvar *)
   42.24  fun new_tfree (tv as (ix,sort), (pairs,used)) =
   42.25 -      let val v = Name.variant used (string_of_indexname ix)
   42.26 +      let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   42.27        in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
   42.28  
   42.29  
    43.1 --- a/src/Tools/eqsubst.ML	Thu Jun 09 15:38:49 2011 +0200
    43.2 +++ b/src/Tools/eqsubst.ML	Thu Jun 09 16:34:49 2011 +0200
    43.3 @@ -179,7 +179,7 @@
    43.4  fun fakefree_badbounds Ts t = 
    43.5      let val (FakeTs,Ts,newnames) = 
    43.6              List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
    43.7 -                           let val newname = Name.variant usednames n
    43.8 +                           let val newname = singleton (Name.variant_list usednames) n
    43.9                             in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   43.10                                 (newname,ty)::Ts, 
   43.11                                 newname::usednames) end)
    44.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Jun 09 15:38:49 2011 +0200
    44.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Jun 09 16:34:49 2011 +0200
    44.3 @@ -96,7 +96,7 @@
    44.4                 Syntax.string_of_term ctxt t);
    44.5  
    44.6    (*** Construct the fixedpoint definition ***)
    44.7 -  val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
    44.8 +  val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
    44.9  
   44.10    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   44.11  
    45.1 --- a/src/ZF/Tools/primrec_package.ML	Thu Jun 09 15:38:49 2011 +0200
    45.2 +++ b/src/ZF/Tools/primrec_package.ML	Thu Jun 09 16:34:49 2011 +0200
    45.3 @@ -139,8 +139,9 @@
    45.4      (** make definition **)
    45.5  
    45.6      (*the recursive argument*)
    45.7 -    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
    45.8 -                        Ind_Syntax.iT)
    45.9 +    val rec_arg =
   45.10 +      Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
   45.11 +        Ind_Syntax.iT)
   45.12  
   45.13      val def_tm = Logic.mk_equals
   45.14                      (subst_bound (rec_arg, fabs),