1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Thu Jun 09 17:46:25 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Thu Jun 09 17:51:49 2011 +0200
     1.3 @@ -855,7 +855,7 @@
     1.4    @{index_ML Name.context: Name.context} \\
     1.5    @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
     1.6    @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
     1.7 -  @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\
     1.8 +  @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
     1.9    \end{mldecls}
    1.10    \begin{mldecls}
    1.11    @{index_ML Variable.names_of: "Proof.context -> Name.context"} \\
    1.12 @@ -878,8 +878,8 @@
    1.13    \item @{ML Name.invents}~@{text "context name n"} produces @{text
    1.14    "n"} fresh names derived from @{text "name"}.
    1.15  
    1.16 -  \item @{ML Name.variants}~@{text "names context"} produces fresh
    1.17 -  variants of @{text "names"}; the result is entered into the context.
    1.18 +  \item @{ML Name.variant}~@{text "name context"} produces a fresh
    1.19 +  variant of @{text "name"}; the result is declared to the context.
    1.20  
    1.21    \item @{ML Variable.names_of}~@{text "ctxt"} retrieves the context
    1.22    of declared type and term variable names.  Projecting a proof
    1.23 @@ -901,7 +901,7 @@
    1.24    @{assert} (list1 = ["a", "b", "c", "d", "e"]);
    1.25  
    1.26    val list2 =
    1.27 -    #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] Name.context);
    1.28 +    #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] Name.context);
    1.29    @{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]);
    1.30  *}
    1.31  
    1.32 @@ -918,7 +918,7 @@
    1.33    @{assert} (list1 = ["d", "e", "f", "g", "h"]);
    1.34  
    1.35    val list2 =
    1.36 -    #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] names);
    1.37 +    #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] names);
    1.38    @{assert} (list2 = ["x", "xa", "aa", "ab", "'aa", "'ab"]);
    1.39  *}
    1.40  

     2.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Jun 09 17:46:25 2011 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Jun 09 17:51:49 2011 +0200
     2.3 @@ -1255,7 +1255,7 @@
     2.4    \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
     2.5    \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
     2.6    \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
     2.7 -  \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
     2.8 +  \indexdef{}{ML}{Name.variant}\verb|Name.variant: string -> Name.context -> string * Name.context| \\
     2.9    \end{mldecls}
    2.10    \begin{mldecls}
    2.11    \indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\
    2.12 @@ -1277,8 +1277,8 @@
    2.13  
    2.14    \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
    2.15  
    2.16 -  \item \verb|Name.variants|~\isa{names\ context} produces fresh
    2.17 -  variants of \isa{names}; the result is entered into the context.
    2.18 +  \item \verb|Name.variant|~\isa{name\ context} produces a fresh
    2.19 +  variant of \isa{name}; the result is declared to the context.
    2.20  
    2.21    \item \verb|Variable.names_of|~\isa{ctxt} retrieves the context
    2.22    of declared type and term variable names.  Projecting a proof
    2.23 @@ -1333,7 +1333,7 @@
    2.24  \ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}b{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    2.25  \isanewline
    2.26  \ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
    2.27 -\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}Name{\isaliteral{2E}{\isachardot}}variants\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ Name{\isaliteral{2E}{\isachardot}}context{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    2.28 +\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}fold{\isaliteral{5F}{\isacharunderscore}}map\ Name{\isaliteral{2E}{\isachardot}}variant\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ Name{\isaliteral{2E}{\isachardot}}context{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    2.29  \ \ %
    2.30  \isaantiq
    2.31  assert{}%
    2.32 @@ -1378,7 +1378,7 @@
    2.33  \ {\isaliteral{28}{\isacharparenleft}}list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}d{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}e{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}f{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}g{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}h{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    2.34  \isanewline
    2.35  \ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
    2.36 -\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}Name{\isaliteral{2E}{\isachardot}}variants\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ names{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    2.37 +\ \ \ \ {\isaliteral{23}{\isacharhash}}{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}fold{\isaliteral{5F}{\isacharunderscore}}map\ Name{\isaliteral{2E}{\isachardot}}variant\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}x{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}\ names{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
    2.38  \ \ %
    2.39  \isaantiq
    2.40  assert{}%

     3.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Jun 09 17:46:25 2011 +0200
     3.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Jun 09 17:51:49 2011 +0200
     3.3 @@ -446,8 +446,7 @@
     3.4        val nctxt = Name.make_context (duplicates (op =) (names_of t []))
     3.5  
     3.6        fun fresh (i, nctxt) = (position_prefix ^ string_of_int i, (i+1, nctxt))
     3.7 -      fun renamed n (i, nctxt) =
     3.8 -        yield_singleton Name.variants n nctxt ||> pair i
     3.9 +      fun renamed n (i, nctxt) = Name.variant n nctxt ||> pair i
    3.10        fun mk_label (name, t) = @{term assert_at} $ Free (name, @{typ bool}) $ t
    3.11  
    3.12        fun unique t =
    3.13 @@ -472,11 +471,11 @@
    3.14          all_names
    3.15          |> map_filter (try (fn n => (n, short_var_name n)))
    3.16          |> split_list
    3.17 -        ||>> (fn names => Name.variants names (Name.make_context all_names))
    3.18 +        ||>> (fn names => fold_map Name.variant names (Name.make_context all_names))
    3.19          |>> Symtab.make o (op ~~)
    3.20  
    3.21        fun rename_free n = the_default n (Symtab.lookup names n)
    3.22 -      fun rename_abs n = yield_singleton Name.variants (short_var_name n)
    3.23 +      fun rename_abs n = Name.variant (short_var_name n)
    3.24  
    3.25        fun rename _ (Free (n, T)) = Free (rename_free n, T)
    3.26          | rename nctxt (Abs (n, T, t)) =

     4.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jun 09 17:46:25 2011 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Jun 09 17:51:49 2011 +0200
     4.3 @@ -200,7 +200,7 @@
     4.4      val ind_sort = if null atomTs then HOLogic.typeS
     4.5        else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
     4.6          ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
     4.7 -    val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
     4.8 +    val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
     4.9      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    4.10      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    4.11  

     5.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Jun 09 17:46:25 2011 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Jun 09 17:51:49 2011 +0200
     5.3 @@ -226,7 +226,7 @@
     5.4      val ind_sort = if null atomTs then HOLogic.typeS
     5.5        else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
     5.6          ("fs_" ^ Long_Name.base_name a)) atoms));
     5.7 -    val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
     5.8 +    val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
     5.9      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    5.10      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    5.11  

     6.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 17:46:25 2011 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 17:51:49 2011 +0200
     6.3 @@ -36,7 +36,7 @@
     6.4    let
     6.5      val (vs, Ts) = split_list (strip_qnt_vars "all" t);
     6.6      val body = strip_qnt_body "all" t;
     6.7 -    val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
     6.8 +    val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
     6.9        (fn Free (v, _) => insert (op =) v | _ => I) body []))
    6.10    in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
    6.11  

     7.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 09 17:46:25 2011 +0200
     7.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 09 17:51:49 2011 +0200
     7.3 @@ -136,7 +136,7 @@
     7.4  fun mk_variables thy prfx xs ty (tab, ctxt) =
     7.5    let
     7.6      val T = mk_type thy prfx ty;
     7.7 -    val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt;
     7.8 +    val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
     7.9      val zs = map (Free o rpair T) ys;
    7.10    in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
    7.11  
    7.12 @@ -779,7 +779,7 @@
    7.13        map_filter (fn s => lookup funs s |>
    7.14          Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
    7.15        split_list ||> split_list;
    7.16 -    val (fs', ctxt') = Name.variants fs ctxt
    7.17 +    val (fs', ctxt') = fold_map Name.variant fs ctxt
    7.18    in
    7.19      (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
    7.20       Element.Fixes (map2 (fn s => fn T =>

     8.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jun 09 17:46:25 2011 +0200
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jun 09 17:51:49 2011 +0200
     8.3 @@ -134,7 +134,7 @@
     8.4  
     8.5      val names = map Long_Name.base_name (the_default tycos (#alt_names info));
     8.6      val (auxnames, _) = Name.make_context names
     8.7 -      |> fold_map (yield_singleton Name.variants o Datatype_Aux.name_of_typ) Us;
     8.8 +      |> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us;
     8.9      val prefix = space_implode "_" names;
    8.10  
    8.11    in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;

     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 17:46:25 2011 +0200
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 17:51:49 2011 +0200
     9.3 @@ -542,7 +542,7 @@
     9.4  fun focus_ex t nctxt =
     9.5    let
     9.6      val ((xs, Ts), t') = apfst split_list (strip_ex t) 
     9.7 -    val (xs', nctxt') = Name.variants xs nctxt;
     9.8 +    val (xs', nctxt') = fold_map Name.variant xs nctxt;
     9.9      val ps' = xs' ~~ Ts;
    9.10      val vs = map Free ps';
    9.11      val t'' = Term.subst_bounds (rev vs, t');

    10.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 17:46:25 2011 +0200
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 17:51:49 2011 +0200
    10.3 @@ -84,8 +84,8 @@
    10.4      val (argTs, resT) = strip_type (fastype_of func)
    10.5      val nctxt =
    10.6        Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
    10.7 -    val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
    10.8 -    val ([resname], nctxt'') = Name.variants ["r"] nctxt'
    10.9 +    val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt
   10.10 +    val (resname, nctxt'') = Name.variant "r" nctxt'
   10.11      val args = map Free (argnames ~~ argTs)
   10.12      val res = Free (resname, resT)
   10.13    in Logic.mk_equals

    11.1 --- a/src/HOL/Tools/primrec.ML	Thu Jun 09 17:46:25 2011 +0200
    11.2 +++ b/src/HOL/Tools/primrec.ML	Thu Jun 09 17:51:49 2011 +0200
    11.3 @@ -38,7 +38,7 @@
    11.4    let
    11.5      val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
    11.6      val body = strip_qnt_body "all" spec;
    11.7 -    val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
    11.8 +    val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
    11.9        (fn Free (v, _) => insert (op =) v | _ => I) body []));
   11.10      val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
   11.11      val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn)

    12.1 --- a/src/Pure/Isar/code.ML	Thu Jun 09 17:46:25 2011 +0200
    12.2 +++ b/src/Pure/Isar/code.ML	Thu Jun 09 17:51:49 2011 +0200
    12.3 @@ -1145,8 +1145,8 @@
    12.4  
    12.5  fun case_cong thy case_const (num_args, (pos, _)) =
    12.6    let
    12.7 -    val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
    12.8 -    val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
    12.9 +    val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
   12.10 +    val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
   12.11      val (ws, vs) = chop pos zs;
   12.12      val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
   12.13      val Ts = binder_types T;

    13.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Jun 09 17:46:25 2011 +0200
    13.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Jun 09 17:51:49 2011 +0200
    13.3 @@ -29,7 +29,7 @@
    13.4  fun variant a ctxt =
    13.5    let
    13.6      val names = Names.get ctxt;
    13.7 -    val ([b], names') = Name.variants [a] names;
    13.8 +    val (b, names') = Name.variant a names;
    13.9      val ctxt' = Names.put names' ctxt;
   13.10    in (b, ctxt') end;
   13.11  

    14.1 --- a/src/Pure/Proof/proofchecker.ML	Thu Jun 09 17:46:25 2011 +0200
    14.2 +++ b/src/Pure/Proof/proofchecker.ML	Thu Jun 09 17:51:49 2011 +0200
    14.3 @@ -100,7 +100,7 @@
    14.4  
    14.5        | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
    14.6            let
    14.7 -            val ([x], names') = Name.variants [s] names;
    14.8 +            val (x, names') = Name.variant s names;
    14.9              val thm = thm_of ((x, T) :: vs, names') Hs prf
   14.10            in
   14.11              Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm

    15.1 --- a/src/Pure/Syntax/syntax_trans.ML	Thu Jun 09 17:46:25 2011 +0200
    15.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Thu Jun 09 17:51:49 2011 +0200
    15.3 @@ -439,7 +439,7 @@
    15.4  (* dependent / nondependent quantifiers *)
    15.5  
    15.6  fun var_abs mark (x, T, b) =
    15.7 -  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
    15.8 +  let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
    15.9    in (x', subst_bound (mark (x', T), b)) end;
   15.10  
   15.11  val variant_abs = var_abs Free;

    16.1 --- a/src/Pure/name.ML	Thu Jun 09 17:46:25 2011 +0200
    16.2 +++ b/src/Pure/name.ML	Thu Jun 09 17:51:49 2011 +0200
    16.3 @@ -24,7 +24,7 @@
    16.4    val invents: context -> string -> int -> string list
    16.5    val names: context -> string -> 'a list -> (string * 'a) list
    16.6    val invent_list: string list -> string -> int -> string list
    16.7 -  val variants: string list -> context -> string list * context
    16.8 +  val variant: string -> context -> string * context
    16.9    val variant_list: string list -> string list -> string list
   16.10    val desymbolize: bool -> string -> string
   16.11  end;
   16.12 @@ -115,7 +115,7 @@
   16.13  
   16.14  (*makes a variant of a name distinct from already used names in a
   16.15    context; preserves a suffix of underscores "_"*)
   16.16 -val variants = fold_map (fn name => fn ctxt =>
   16.17 +fun variant name ctxt =
   16.18    let
   16.19      fun vary x =
   16.20        (case declared ctxt x of
   16.21 @@ -133,9 +133,9 @@
   16.22              |> x0 <> x' ? declare_renaming (x0, x')
   16.23              |> declare x';
   16.24          in (x', ctxt') end;
   16.25 -  in (x' ^ replicate_string n "_", ctxt') end);
   16.26 +  in (x' ^ replicate_string n "_", ctxt') end;
   16.27  
   16.28 -fun variant_list used names = #1 (make_context used |> variants names);
   16.29 +fun variant_list used names = #1 (make_context used |> fold_map variant names);
   16.30  
   16.31  
   16.32  (* names conforming to typical requirements of identifiers in the world outside *)

    17.1 --- a/src/Pure/proofterm.ML	Thu Jun 09 17:46:25 2011 +0200
    17.2 +++ b/src/Pure/proofterm.ML	Thu Jun 09 17:51:49 2011 +0200
    17.3 @@ -657,7 +657,7 @@
    17.4        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    17.5      val used = Name.context
    17.6        |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
    17.7 -    val fmap = fs ~~ #1 (Name.variants (map fst fs) used);
    17.8 +    val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
    17.9      fun thaw (f as (a, S)) =
   17.10        (case AList.lookup (op =) fmap f of
   17.11          NONE => TFree f

    18.1 --- a/src/Pure/raw_simplifier.ML	Thu Jun 09 17:46:25 2011 +0200
    18.2 +++ b/src/Pure/raw_simplifier.ML	Thu Jun 09 17:51:49 2011 +0200
    18.3 @@ -305,7 +305,7 @@
    18.4  fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
    18.5    let
    18.6      val names = Term.declare_term_names t Name.context;
    18.7 -    val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
    18.8 +    val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names));
    18.9      fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
   18.10    in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
   18.11  

    19.1 --- a/src/Pure/term.ML	Thu Jun 09 17:46:25 2011 +0200
    19.2 +++ b/src/Pure/term.ML	Thu Jun 09 17:51:49 2011 +0200
    19.3 @@ -514,7 +514,8 @@
    19.4  val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
    19.5  
    19.6  fun variant_frees t frees =
    19.7 -  fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
    19.8 +  fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
    19.9 +    map snd frees;
   19.10  
   19.11  fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
   19.12  
   19.13 @@ -705,7 +706,7 @@
   19.14      fun strip_abs t (0, used) = (([], t), (0, used))
   19.15        | strip_abs (Abs (v, T, t)) (k, used) =
   19.16            let
   19.17 -            val ([v'], used') = Name.variants [v] used;
   19.18 +            val (v', used') = Name.variant v used;
   19.19              val t' = subst_bound (Free (v', T), t);
   19.20              val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
   19.21            in (((v', T) :: vs, t''), (k', used'')) end
   19.22 @@ -713,7 +714,7 @@
   19.23      fun expand_eta [] t _ = ([], t)
   19.24        | expand_eta (T::Ts) t used =
   19.25            let
   19.26 -            val ([v], used') = Name.variants [""] used;
   19.27 +            val (v, used') = Name.variant "" used;
   19.28              val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
   19.29            in ((v, T) :: vs, t') end;
   19.30      val ((vs1, t'), (k', used')) = strip_abs t (k, used);

    20.1 --- a/src/Pure/term_subst.ML	Thu Jun 09 17:46:25 2011 +0200
    20.2 +++ b/src/Pure/term_subst.ML	Thu Jun 09 17:51:49 2011 +0200
    20.3 @@ -163,7 +163,7 @@
    20.4  fun zero_var_inst vars =
    20.5    fold (fn v as ((x, i), X) => fn (inst, used) =>
    20.6      let
    20.7 -      val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
    20.8 +      val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
    20.9      in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
   20.10    vars ([], Name.context) |> #1;
   20.11  

    21.1 --- a/src/Pure/type.ML	Thu Jun 09 17:46:25 2011 +0200
    21.2 +++ b/src/Pure/type.ML	Thu Jun 09 17:51:49 2011 +0200
    21.3 @@ -345,7 +345,7 @@
    21.4        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    21.5      val used = Name.context
    21.6        |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
    21.7 -    val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used));
    21.8 +    val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
    21.9      fun thaw (f as (_, S)) =
   21.10        (case AList.lookup (op =) fmap f of
   21.11          NONE => TFree f

    22.1 --- a/src/Pure/variable.ML	Thu Jun 09 17:46:25 2011 +0200
    22.2 +++ b/src/Pure/variable.ML	Thu Jun 09 17:51:49 2011 +0200
    22.3 @@ -255,7 +255,7 @@
    22.4  fun variant_frees ctxt ts frees =
    22.5    let
    22.6      val names = names_of (fold declare_names ts ctxt);
    22.7 -    val xs = fst (Name.variants (map #1 frees) names);
    22.8 +    val xs = fst (fold_map Name.variant (map #1 frees) names);
    22.9    in xs ~~ map snd frees end;
   22.10  
   22.11  
   22.12 @@ -365,7 +365,7 @@
   22.13      val xs = map check_name bs;
   22.14      val names = names_of ctxt;
   22.15      val (xs', names') =
   22.16 -      if is_body ctxt then Name.variants xs names |>> map Name.skolem
   22.17 +      if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem
   22.18        else (xs, fold Name.declare xs names);
   22.19    in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
   22.20  
   22.21 @@ -373,7 +373,7 @@
   22.22    let
   22.23      val names = names_of ctxt;
   22.24      val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
   22.25 -    val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
   22.26 +    val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
   22.27    in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
   22.28  
   22.29  end;

    23.1 --- a/src/Tools/Code/code_haskell.ML	Thu Jun 09 17:46:25 2011 +0200
    23.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Jun 09 17:51:49 2011 +0200
    23.3 @@ -264,13 +264,12 @@
    23.4    let
    23.5      fun namify_fun upper base (nsp_fun, nsp_typ) =
    23.6        let
    23.7 -        val (base', nsp_fun') = yield_singleton Name.variants
    23.8 -          (if upper then first_upper base else base) nsp_fun;
    23.9 +        val (base', nsp_fun') =
   23.10 +          Name.variant (if upper then first_upper base else base) nsp_fun;
   23.11        in (base', (nsp_fun', nsp_typ)) end;
   23.12      fun namify_typ base (nsp_fun, nsp_typ) =
   23.13        let
   23.14 -        val (base', nsp_typ') = yield_singleton Name.variants
   23.15 -          (first_upper base) nsp_typ
   23.16 +        val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
   23.17        in (base', (nsp_fun, nsp_typ')) end;
   23.18      fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
   23.19        | namify_stmt (Code_Thingol.Fun _) = namify_fun false

    24.1 --- a/src/Tools/Code/code_ml.ML	Thu Jun 09 17:46:25 2011 +0200
    24.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jun 09 17:51:49 2011 +0200
    24.3 @@ -715,12 +715,12 @@
    24.4    let
    24.5      fun namify_const upper base (nsp_const, nsp_type) =
    24.6        let
    24.7 -        val (base', nsp_const') = yield_singleton Name.variants
    24.8 -          (if upper then first_upper base else base) nsp_const
    24.9 +        val (base', nsp_const') =
   24.10 +          Name.variant (if upper then first_upper base else base) nsp_const
   24.11        in (base', (nsp_const', nsp_type)) end;
   24.12      fun namify_type base (nsp_const, nsp_type) =
   24.13        let
   24.14 -        val (base', nsp_type') = yield_singleton Name.variants base nsp_type
   24.15 +        val (base', nsp_type') = Name.variant base nsp_type
   24.16        in (base', (nsp_const, nsp_type')) end;
   24.17      fun namify_stmt (Code_Thingol.Fun _) = namify_const false
   24.18        | namify_stmt (Code_Thingol.Datatype _) = namify_type

    25.1 --- a/src/Tools/Code/code_namespace.ML	Thu Jun 09 17:46:25 2011 +0200
    25.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Jun 09 17:51:49 2011 +0200
    25.3 @@ -46,8 +46,7 @@
    25.4    let
    25.5      fun alias_fragments name = case module_alias name
    25.6       of SOME name' => Long_Name.explode name'
    25.7 -      | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
    25.8 -          (Long_Name.explode name);
    25.9 +      | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
   25.10      val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
   25.11    in
   25.12      fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))

    26.1 --- a/src/Tools/Code/code_printer.ML	Thu Jun 09 17:46:25 2011 +0200
    26.2 +++ b/src/Tools/Code/code_printer.ML	Thu Jun 09 17:51:49 2011 +0200
    26.3 @@ -165,7 +165,7 @@
    26.4  
    26.5  fun intro_vars names (namemap, namectxt) =
    26.6    let
    26.7 -    val (names', namectxt') = Name.variants names namectxt;
    26.8 +    val (names', namectxt') = fold_map Name.variant names namectxt;
    26.9      val namemap' = fold2 (curry Symtab.update) names names' namemap;
   26.10    in (namemap', namectxt') end;
   26.11  
   26.12 @@ -186,7 +186,7 @@
   26.13      val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
   26.14      val x = singleton (Name.variant_list (map_filter I fished1)) "x";
   26.15      val fished2 = map_index (fillup_param x) fished1;
   26.16 -    val (fished3, _) = Name.variants fished2 Name.context;
   26.17 +    val (fished3, _) = fold_map Name.variant fished2 Name.context;
   26.18      val vars' = intro_vars fished3 vars;
   26.19    in map (lookup_var vars') fished3 end;
   26.20  

    27.1 --- a/src/Tools/Code/code_scala.ML	Thu Jun 09 17:46:25 2011 +0200
    27.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jun 09 17:51:49 2011 +0200
    27.3 @@ -294,16 +294,16 @@
    27.4        in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
    27.5      fun namify_class base ((nsp_class, nsp_object), nsp_common) =
    27.6        let
    27.7 -        val (base', nsp_class') = yield_singleton Name.variants base nsp_class
    27.8 +        val (base', nsp_class') = Name.variant base nsp_class
    27.9        in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   27.10      fun namify_object base ((nsp_class, nsp_object), nsp_common) =
   27.11        let
   27.12 -        val (base', nsp_object') = yield_singleton Name.variants base nsp_object
   27.13 +        val (base', nsp_object') = Name.variant base nsp_object
   27.14        in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   27.15      fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
   27.16        let
   27.17          val (base', nsp_common') =
   27.18 -          yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
   27.19 +          Name.variant (if upper then first_upper base else base) nsp_common
   27.20        in
   27.21          (base',
   27.22            ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))

    28.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jun 09 17:46:25 2011 +0200
    28.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jun 09 17:51:49 2011 +0200
    28.3 @@ -354,7 +354,7 @@
    28.4  
    28.5  fun add_variant update (thing, name) (tab, used) =
    28.6    let
    28.7 -    val (name', used') = yield_singleton Name.variants name used;
    28.8 +    val (name', used') = Name.variant name used;
    28.9      val tab' = update (thing, name') tab;
   28.10    in (tab', used') end;
   28.11  

    29.1 --- a/src/Tools/induct.ML	Thu Jun 09 17:46:25 2011 +0200
    29.2 +++ b/src/Tools/induct.ML	Thu Jun 09 17:51:49 2011 +0200
    29.3 @@ -692,7 +692,7 @@
    29.4        | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
    29.5        | add (SOME (NONE, (t, _))) ctxt =
    29.6            let
    29.7 -            val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
    29.8 +            val (s, _) = Name.variant "x" (Variable.names_of ctxt);
    29.9              val ([(lhs, (_, th))], ctxt') =
   29.10                Local_Defs.add_defs [((Binding.name s, NoSyn),
   29.11                  (Thm.empty_binding, t))] ctxt