--- a/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jun 09 17:46:25 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jun 09 17:51:49 2011 +0200
@@ -855,7 +855,7 @@
@{index_ML Name.context: Name.context} \\
@{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
@{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
- @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\
+ @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML Variable.names_of: "Proof.context -> Name.context"} \\
@@ -878,8 +878,8 @@
\item @{ML Name.invents}~@{text "context name n"} produces @{text
"n"} fresh names derived from @{text "name"}.
- \item @{ML Name.variants}~@{text "names context"} produces fresh
- variants of @{text "names"}; the result is entered into the context.
+ \item @{ML Name.variant}~@{text "name context"} produces a fresh
+ variant of @{text "name"}; the result is declared to the context.
\item @{ML Variable.names_of}~@{text "ctxt"} retrieves the context
of declared type and term variable names. Projecting a proof
@@ -901,7 +901,7 @@
@{assert} (list1 = ["a", "b", "c", "d", "e"]);
val list2 =
- #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] Name.context);
+ #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] Name.context);
@{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]);
*}
@@ -918,7 +918,7 @@
@{assert} (list1 = ["d", "e", "f", "g", "h"]);
val list2 =
- #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] names);
+ #1 (fold_map Name.variant ["x", "x", "a", "a", "'a", "'a"] names);
@{assert} (list2 = ["x", "xa", "aa", "ab", "'aa", "'ab"]);
*}
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Jun 09 17:46:25 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Jun 09 17:51:49 2011 +0200
@@ -1255,7 +1255,7 @@
\indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
\indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
\indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
- \indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
+ \indexdef{}{ML}{Name.variant}\verb|Name.variant: string -> Name.context -> string * Name.context| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\
@@ -1277,8 +1277,8 @@
\item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
- \item \verb|Name.variants|~\isa{names\ context} produces fresh
- variants of \isa{names}; the result is entered into the context.
+ \item \verb|Name.variant|~\isa{name\ context} produces a fresh
+ variant of \isa{name}; the result is declared to the context.
\item \verb|Variable.names_of|~\isa{ctxt} retrieves the context
of declared type and term variable names. Projecting a proof
@@ -1333,7 +1333,7 @@
\ {\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
\isanewline
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ {\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
+\ \ \ \ {\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
\ \ %
\isaantiq
assert{}%
@@ -1378,7 +1378,7 @@
\ {\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
\isanewline
\ \ val\ list{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ {\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
+\ \ \ \ {\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
\ \ %
\isaantiq
assert{}%
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Thu Jun 09 17:51:49 2011 +0200
@@ -446,8 +446,7 @@
val nctxt = Name.make_context (duplicates (op =) (names_of t []))
fun fresh (i, nctxt) = (position_prefix ^ string_of_int i, (i+1, nctxt))
- fun renamed n (i, nctxt) =
- yield_singleton Name.variants n nctxt ||> pair i
+ fun renamed n (i, nctxt) = Name.variant n nctxt ||> pair i
fun mk_label (name, t) = @{term assert_at} $ Free (name, @{typ bool}) $ t
fun unique t =
@@ -472,11 +471,11 @@
all_names
|> map_filter (try (fn n => (n, short_var_name n)))
|> split_list
- ||>> (fn names => Name.variants names (Name.make_context all_names))
+ ||>> (fn names => fold_map Name.variant names (Name.make_context all_names))
|>> Symtab.make o (op ~~)
fun rename_free n = the_default n (Symtab.lookup names n)
- fun rename_abs n = yield_singleton Name.variants (short_var_name n)
+ fun rename_abs n = Name.variant (short_var_name n)
fun rename _ (Free (n, T)) = Free (rename_free n, T)
| rename nctxt (Abs (n, T, t)) =
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Jun 09 17:51:49 2011 +0200
@@ -200,7 +200,7 @@
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
- val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
+ val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Jun 09 17:51:49 2011 +0200
@@ -226,7 +226,7 @@
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
("fs_" ^ Long_Name.base_name a)) atoms));
- val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
+ val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 17:51:49 2011 +0200
@@ -36,7 +36,7 @@
let
val (vs, Ts) = split_list (strip_qnt_vars "all" t);
val body = strip_qnt_body "all" t;
- val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
+ val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []))
in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 09 17:51:49 2011 +0200
@@ -136,7 +136,7 @@
fun mk_variables thy prfx xs ty (tab, ctxt) =
let
val T = mk_type thy prfx ty;
- val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt;
+ val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
val zs = map (Free o rpair T) ys;
in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
@@ -779,7 +779,7 @@
map_filter (fn s => lookup funs s |>
Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
split_list ||> split_list;
- val (fs', ctxt') = Name.variants fs ctxt
+ val (fs', ctxt') = fold_map Name.variant fs ctxt
in
(fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
Element.Fixes (map2 (fn s => fn T =>
--- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Jun 09 17:51:49 2011 +0200
@@ -134,7 +134,7 @@
val names = map Long_Name.base_name (the_default tycos (#alt_names info));
val (auxnames, _) = Name.make_context names
- |> fold_map (yield_singleton Name.variants o Datatype_Aux.name_of_typ) Us;
+ |> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us;
val prefix = space_implode "_" names;
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 17:51:49 2011 +0200
@@ -542,7 +542,7 @@
fun focus_ex t nctxt =
let
val ((xs, Ts), t') = apfst split_list (strip_ex t)
- val (xs', nctxt') = Name.variants xs nctxt;
+ val (xs', nctxt') = fold_map Name.variant xs nctxt;
val ps' = xs' ~~ Ts;
val vs = map Free ps';
val t'' = Term.subst_bounds (rev vs, t');
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 17:51:49 2011 +0200
@@ -84,8 +84,8 @@
val (argTs, resT) = strip_type (fastype_of func)
val nctxt =
Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
- val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
- val ([resname], nctxt'') = Name.variants ["r"] nctxt'
+ val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt
+ val (resname, nctxt'') = Name.variant "r" nctxt'
val args = map Free (argnames ~~ argTs)
val res = Free (resname, resT)
in Logic.mk_equals
--- a/src/HOL/Tools/primrec.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Tools/primrec.ML Thu Jun 09 17:51:49 2011 +0200
@@ -38,7 +38,7 @@
let
val (vs, Ts) = split_list (strip_qnt_vars "all" spec);
val body = strip_qnt_body "all" spec;
- val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
+ val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
(fn Free (v, _) => insert (op =) v | _ => I) body []));
val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn)
--- a/src/Pure/Isar/code.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/Isar/code.ML Thu Jun 09 17:51:49 2011 +0200
@@ -1145,8 +1145,8 @@
fun case_cong thy case_const (num_args, (pos, _)) =
let
- val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
- val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
+ val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context;
+ val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt;
val (ws, vs) = chop pos zs;
val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
val Ts = binder_types T;
--- a/src/Pure/ML/ml_antiquote.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Thu Jun 09 17:51:49 2011 +0200
@@ -29,7 +29,7 @@
fun variant a ctxt =
let
val names = Names.get ctxt;
- val ([b], names') = Name.variants [a] names;
+ val (b, names') = Name.variant a names;
val ctxt' = Names.put names' ctxt;
in (b, ctxt') end;
--- a/src/Pure/Proof/proofchecker.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/Proof/proofchecker.ML Thu Jun 09 17:51:49 2011 +0200
@@ -100,7 +100,7 @@
| thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
let
- val ([x], names') = Name.variants [s] names;
+ val (x, names') = Name.variant s names;
val thm = thm_of ((x, T) :: vs, names') Hs prf
in
Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
--- a/src/Pure/Syntax/syntax_trans.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Thu Jun 09 17:51:49 2011 +0200
@@ -439,7 +439,7 @@
(* dependent / nondependent quantifiers *)
fun var_abs mark (x, T, b) =
- let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
+ let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
in (x', subst_bound (mark (x', T), b)) end;
val variant_abs = var_abs Free;
--- a/src/Pure/name.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/name.ML Thu Jun 09 17:51:49 2011 +0200
@@ -24,7 +24,7 @@
val invents: context -> string -> int -> string list
val names: context -> string -> 'a list -> (string * 'a) list
val invent_list: string list -> string -> int -> string list
- val variants: string list -> context -> string list * context
+ val variant: string -> context -> string * context
val variant_list: string list -> string list -> string list
val desymbolize: bool -> string -> string
end;
@@ -115,7 +115,7 @@
(*makes a variant of a name distinct from already used names in a
context; preserves a suffix of underscores "_"*)
-val variants = fold_map (fn name => fn ctxt =>
+fun variant name ctxt =
let
fun vary x =
(case declared ctxt x of
@@ -133,9 +133,9 @@
|> x0 <> x' ? declare_renaming (x0, x')
|> declare x';
in (x', ctxt') end;
- in (x' ^ replicate_string n "_", ctxt') end);
+ in (x' ^ replicate_string n "_", ctxt') end;
-fun variant_list used names = #1 (make_context used |> variants names);
+fun variant_list used names = #1 (make_context used |> fold_map variant names);
(* names conforming to typical requirements of identifiers in the world outside *)
--- a/src/Pure/proofterm.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/proofterm.ML Thu Jun 09 17:51:49 2011 +0200
@@ -657,7 +657,7 @@
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
- val fmap = fs ~~ #1 (Name.variants (map fst fs) used);
+ val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
fun thaw (f as (a, S)) =
(case AList.lookup (op =) fmap f of
NONE => TFree f
--- a/src/Pure/raw_simplifier.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Thu Jun 09 17:51:49 2011 +0200
@@ -305,7 +305,7 @@
fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
let
val names = Term.declare_term_names t Name.context;
- val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
+ val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names));
fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
--- a/src/Pure/term.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/term.ML Thu Jun 09 17:51:49 2011 +0200
@@ -514,7 +514,8 @@
val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
fun variant_frees t frees =
- fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
+ fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
+ map snd frees;
fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*)
@@ -705,7 +706,7 @@
fun strip_abs t (0, used) = (([], t), (0, used))
| strip_abs (Abs (v, T, t)) (k, used) =
let
- val ([v'], used') = Name.variants [v] used;
+ val (v', used') = Name.variant v used;
val t' = subst_bound (Free (v', T), t);
val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
in (((v', T) :: vs, t''), (k', used'')) end
@@ -713,7 +714,7 @@
fun expand_eta [] t _ = ([], t)
| expand_eta (T::Ts) t used =
let
- val ([v], used') = Name.variants [""] used;
+ val (v, used') = Name.variant "" used;
val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
in ((v, T) :: vs, t') end;
val ((vs1, t'), (k', used')) = strip_abs t (k, used);
--- a/src/Pure/term_subst.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/term_subst.ML Thu Jun 09 17:51:49 2011 +0200
@@ -163,7 +163,7 @@
fun zero_var_inst vars =
fold (fn v as ((x, i), X) => fn (inst, used) =>
let
- val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
+ val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
vars ([], Name.context) |> #1;
--- a/src/Pure/type.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/type.ML Thu Jun 09 17:51:49 2011 +0200
@@ -345,7 +345,7 @@
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
- val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used));
+ val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
fun thaw (f as (_, S)) =
(case AList.lookup (op =) fmap f of
NONE => TFree f
--- a/src/Pure/variable.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/variable.ML Thu Jun 09 17:51:49 2011 +0200
@@ -255,7 +255,7 @@
fun variant_frees ctxt ts frees =
let
val names = names_of (fold declare_names ts ctxt);
- val xs = fst (Name.variants (map #1 frees) names);
+ val xs = fst (fold_map Name.variant (map #1 frees) names);
in xs ~~ map snd frees end;
@@ -365,7 +365,7 @@
val xs = map check_name bs;
val names = names_of ctxt;
val (xs', names') =
- if is_body ctxt then Name.variants xs names |>> map Name.skolem
+ if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem
else (xs, fold Name.declare xs names);
in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
@@ -373,7 +373,7 @@
let
val names = names_of ctxt;
val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
- val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
+ val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
end;
--- a/src/Tools/Code/code_haskell.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML Thu Jun 09 17:51:49 2011 +0200
@@ -264,13 +264,12 @@
let
fun namify_fun upper base (nsp_fun, nsp_typ) =
let
- val (base', nsp_fun') = yield_singleton Name.variants
- (if upper then first_upper base else base) nsp_fun;
+ val (base', nsp_fun') =
+ Name.variant (if upper then first_upper base else base) nsp_fun;
in (base', (nsp_fun', nsp_typ)) end;
fun namify_typ base (nsp_fun, nsp_typ) =
let
- val (base', nsp_typ') = yield_singleton Name.variants
- (first_upper base) nsp_typ
+ val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
in (base', (nsp_fun, nsp_typ')) end;
fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
| namify_stmt (Code_Thingol.Fun _) = namify_fun false
--- a/src/Tools/Code/code_ml.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Jun 09 17:51:49 2011 +0200
@@ -715,12 +715,12 @@
let
fun namify_const upper base (nsp_const, nsp_type) =
let
- val (base', nsp_const') = yield_singleton Name.variants
- (if upper then first_upper base else base) nsp_const
+ val (base', nsp_const') =
+ Name.variant (if upper then first_upper base else base) nsp_const
in (base', (nsp_const', nsp_type)) end;
fun namify_type base (nsp_const, nsp_type) =
let
- val (base', nsp_type') = yield_singleton Name.variants base nsp_type
+ val (base', nsp_type') = Name.variant base nsp_type
in (base', (nsp_const, nsp_type')) end;
fun namify_stmt (Code_Thingol.Fun _) = namify_const false
| namify_stmt (Code_Thingol.Datatype _) = namify_type
--- a/src/Tools/Code/code_namespace.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Tools/Code/code_namespace.ML Thu Jun 09 17:51:49 2011 +0200
@@ -46,8 +46,7 @@
let
fun alias_fragments name = case module_alias name
of SOME name' => Long_Name.explode name'
- | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
- (Long_Name.explode name);
+ | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
in
fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
--- a/src/Tools/Code/code_printer.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Jun 09 17:51:49 2011 +0200
@@ -165,7 +165,7 @@
fun intro_vars names (namemap, namectxt) =
let
- val (names', namectxt') = Name.variants names namectxt;
+ val (names', namectxt') = fold_map Name.variant names namectxt;
val namemap' = fold2 (curry Symtab.update) names names' namemap;
in (namemap', namectxt') end;
@@ -186,7 +186,7 @@
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
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 (fished3, _) = fold_map Name.variant fished2 Name.context;
val vars' = intro_vars fished3 vars;
in map (lookup_var vars') fished3 end;
--- a/src/Tools/Code/code_scala.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Jun 09 17:51:49 2011 +0200
@@ -294,16 +294,16 @@
in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
fun namify_class base ((nsp_class, nsp_object), nsp_common) =
let
- val (base', nsp_class') = yield_singleton Name.variants base nsp_class
+ val (base', nsp_class') = Name.variant base nsp_class
in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
fun namify_object base ((nsp_class, nsp_object), nsp_common) =
let
- val (base', nsp_object') = yield_singleton Name.variants base nsp_object
+ val (base', nsp_object') = Name.variant base nsp_object
in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
let
val (base', nsp_common') =
- yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
+ Name.variant (if upper then first_upper base else base) nsp_common
in
(base',
((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
--- a/src/Tools/Code/code_thingol.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Jun 09 17:51:49 2011 +0200
@@ -354,7 +354,7 @@
fun add_variant update (thing, name) (tab, used) =
let
- val (name', used') = yield_singleton Name.variants name used;
+ val (name', used') = Name.variant name used;
val tab' = update (thing, name') tab;
in (tab', used') end;
--- a/src/Tools/induct.ML Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Tools/induct.ML Thu Jun 09 17:51:49 2011 +0200
@@ -692,7 +692,7 @@
| add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
| add (SOME (NONE, (t, _))) ctxt =
let
- val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
+ val (s, _) = Name.variant "x" (Variable.names_of ctxt);
val ([(lhs, (_, th))], ctxt') =
Local_Defs.add_defs [((Binding.name s, NoSyn),
(Thm.empty_binding, t))] ctxt