--- a/doc-src/IsarImplementation/Thy/Prelim.thy Wed Jun 08 22:16:21 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Jun 09 20:22:22 2011 +0200
@@ -854,7 +854,7 @@
@{index_ML_type Name.context} \\
@{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.invent: "Name.context -> string -> int -> string list"} \\
@{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
\end{mldecls}
\begin{mldecls}
@@ -875,7 +875,7 @@
\item @{ML Name.declare}~@{text "name"} enters a used name into the
context.
- \item @{ML Name.invents}~@{text "context name n"} produces @{text
+ \item @{ML Name.invent}~@{text "context name n"} produces @{text
"n"} fresh names derived from @{text "name"}.
\item @{ML Name.variant}~@{text "name context"} produces a fresh
@@ -897,7 +897,7 @@
fresh names from the initial @{ML Name.context}. *}
ML {*
- val list1 = Name.invents Name.context "a" 5;
+ val list1 = Name.invent Name.context "a" 5;
@{assert} (list1 = ["a", "b", "c", "d", "e"]);
val list2 =
@@ -914,7 +914,7 @@
ML {*
val names = Variable.names_of @{context};
- val list1 = Name.invents names "a" 5;
+ val list1 = Name.invent names "a" 5;
@{assert} (list1 = ["d", "e", "f", "g", "h"]);
val list2 =
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Wed Jun 08 22:16:21 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Thu Jun 09 20:22:22 2011 +0200
@@ -1254,7 +1254,7 @@
\indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
\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.invent}\verb|Name.invent: Name.context -> string -> int -> string list| \\
\indexdef{}{ML}{Name.variant}\verb|Name.variant: string -> Name.context -> string * Name.context| \\
\end{mldecls}
\begin{mldecls}
@@ -1275,7 +1275,7 @@
\item \verb|Name.declare|~\isa{name} enters a used name into the
context.
- \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
+ \item \verb|Name.invent|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
\item \verb|Name.variant|~\isa{name\ context} produces a fresh
variant of \isa{name}; the result is declared to the context.
@@ -1325,7 +1325,7 @@
\isatagML
\isacommand{ML}\isamarkupfalse%
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
-\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invents\ Name{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invent\ Name{\isaliteral{2E}{\isachardot}}context\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
@@ -1370,7 +1370,7 @@
\endisaantiq
{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\isanewline
-\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invents\ names\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ Name{\isaliteral{2E}{\isachardot}}invent\ names\ {\isaliteral{22}{\isachardoublequote}}a{\isaliteral{22}{\isachardoublequote}}\ {\isadigit{5}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
\ \ %
\isaantiq
assert{}%
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Thu Jun 09 20:22:22 2011 +0200
@@ -86,7 +86,7 @@
SOME type_name => (((name, type_name), log_ex name type_name), thy)
| NONE =>
let
- val args = map (rpair dummyS) (Name.invents Name.context "'a" arity)
+ val args = map (rpair dummyS) (Name.invent Name.context "'a" arity)
val (T, thy') =
Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
val type_name = fst (Term.dest_Type T)
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Thu Jun 09 20:22:22 2011 +0200
@@ -23,7 +23,7 @@
fun trans_rules name2 name1 n mx =
let
- val vnames = Name.invents Name.context "a" n
+ val vnames = Name.invent Name.context "a" n
val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
in
[Syntax.Parse_Print_Rule
--- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Jun 09 20:22:22 2011 +0200
@@ -407,7 +407,7 @@
fun inter_sort m = map (fn xs => nth xs m) raw_vss
|> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
val sorts = map inter_sort ms;
- val vs = Name.names Name.context Name.aT sorts;
+ val vs = Name.invent_names Name.context Name.aT sorts;
fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
(TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
--- a/src/HOL/Tools/Function/fun.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/Function/fun.ML Thu Jun 09 20:22:22 2011 +0200
@@ -64,7 +64,7 @@
val (argTs, rT) = chop n (binder_types fT)
|> apsnd (fn Ts => Ts ---> body_type fT)
- val qs = map Free (Name.invents Name.context "a" n ~~ argTs)
+ val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
in
HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
Const ("HOL.undefined", rT))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Jun 09 20:22:22 2011 +0200
@@ -129,7 +129,7 @@
fun declare_names s xs ctxt =
let
- val res = Name.names ctxt s xs
+ val res = Name.invent_names ctxt s xs
in (res, fold Name.declare (map fst res) ctxt) end
fun split_all_pairs thy th =
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 09 20:22:22 2011 +0200
@@ -67,7 +67,7 @@
fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
let
- val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys))
+ val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
$ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Jun 09 20:22:22 2011 +0200
@@ -214,7 +214,7 @@
val tTs = (map o apsnd) termifyT simple_tTs;
val is_rec = exists is_some ks;
val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
- val vs = Name.names Name.context "x" (map snd simple_tTs);
+ val vs = Name.invent_names Name.context "x" (map snd simple_tTs);
val tc = HOLogic.mk_return T @{typ Random.seed}
(HOLogic.mk_valtermify_app c vs simpleT);
val t = HOLogic.mk_ST
--- a/src/HOL/Tools/code_evaluation.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Thu Jun 09 20:22:22 2011 +0200
@@ -57,7 +57,7 @@
fun mk_term_of_eq thy ty (c, (_, tys)) =
let
val t = list_comb (Const (c, tys ---> ty),
- map Free (Name.names Name.context "a" tys));
+ map Free (Name.invent_names Name.context "a" tys));
val (arg, rhs) =
pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
(t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
--- a/src/HOL/Tools/enriched_type.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/enriched_type.ML Thu Jun 09 20:22:22 2011 +0200
@@ -98,7 +98,7 @@
val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
fun invents n k nctxt =
let
- val names = Name.invents nctxt n k;
+ val names = Name.invent nctxt n k;
in (names, fold Name.declare names nctxt) end;
val ((names21, names32), nctxt) = Variable.names_of ctxt
|> invents "f" (length Ts21)
@@ -120,7 +120,7 @@
val mapper31 = mk_mapper T3 T1 args31;
val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(HOLogic.mk_comp (mapper21, mapper32), mapper31);
- val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3)
+ val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(mapper21 $ (mapper32 $ x), mapper31 $ x);
val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
--- a/src/HOL/Tools/record.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/record.ML Thu Jun 09 20:22:22 2011 +0200
@@ -1801,7 +1801,7 @@
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
val T = Type (tyco, map TFree vs);
val Tm = termifyT T;
- val params = Name.names Name.context "x" Ts;
+ val params = Name.invent_names Name.context "x" Ts;
val lhs = HOLogic.mk_random T size;
val tc = HOLogic.mk_return Tm @{typ Random.seed}
(HOLogic.mk_valtermify_app extN params T);
@@ -1820,7 +1820,7 @@
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
val T = Type (tyco, map TFree vs);
val test_function = Free ("f", termifyT T --> @{typ "term list option"});
- val params = Name.names Name.context "x" Ts;
+ val params = Name.invent_names Name.context "x" Ts;
fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
--> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
fun mk_full_exhaustive T =
--- a/src/HOL/Typerep.thy Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Typerep.thy Thu Jun 09 20:22:22 2011 +0200
@@ -47,7 +47,7 @@
fun add_typerep tyco thy =
let
val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
- val vs = Name.names Name.context "'a" sorts;
+ val vs = Name.invent_names Name.context "'a" sorts;
val ty = Type (tyco, map TFree vs);
val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
$ Free ("T", Term.itselfT ty);
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jun 09 20:22:22 2011 +0200
@@ -749,7 +749,7 @@
let
val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params)
val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes
- (Name.invents (Variable.names_of ctxt') Name.uu (length Ts - length params))
+ (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params))
val params' = (more_names @ param_names) ~~ Ts
in
trace_ex ctxt'' params' atoms (discr initems) n hist
--- a/src/Pure/Isar/class.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/Isar/class.ML Thu Jun 09 20:22:22 2011 +0200
@@ -426,7 +426,7 @@
(raw_tyco, raw_sorts, raw_sort)) raw_tycos;
val tycos = map #1 all_arities;
val (_, sorts, sort) = hd all_arities;
- val vs = Name.names Name.context Name.aT sorts;
+ val vs = Name.invent_names Name.context Name.aT sorts;
in (tycos, vs, sort) end;
--- a/src/Pure/Isar/code.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/Isar/code.ML Thu Jun 09 20:22:22 2011 +0200
@@ -433,7 +433,7 @@
in (c, (vs'', binder_types ty')) end;
val c' :: cs' = map (analyze_constructor thy) cs;
val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
- val vs = Name.names Name.context Name.aT sorts;
+ val vs = Name.invent_names Name.context Name.aT sorts;
val cs''' = map (inst vs) cs'';
in (tyco, (vs, rev cs''')) end;
@@ -444,7 +444,7 @@
fun get_type thy tyco = case get_type_entry thy tyco
of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
| NONE => arity_number thy tyco
- |> Name.invents Name.context Name.aT
+ |> Name.invent Name.context Name.aT
|> map (rpair [])
|> rpair []
|> rpair false;
@@ -779,7 +779,7 @@
fun inter_sorts vs =
fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
val sorts = map_transpose inter_sorts vss;
- val vts = Name.names Name.context Name.aT sorts;
+ val vts = Name.invent_names Name.context Name.aT sorts;
val thms' =
map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
--- a/src/Pure/Isar/specification.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/Isar/specification.ML Thu Jun 09 20:22:22 2011 +0200
@@ -93,7 +93,7 @@
(case duplicates (op =) commons of [] => ()
| dups => error ("Duplicate local variables " ^ commas_quote dups));
val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
- val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
+ val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
--- a/src/Pure/Proof/proof_rewrite_rules.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 09 20:22:22 2011 +0200
@@ -200,7 +200,7 @@
fun rew_term Ts t =
let
val frees =
- map Free (Name.invents (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
+ map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
val t' = r (subst_bounds (frees, t));
fun strip [] t = t
| strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
--- a/src/Pure/Syntax/syntax_ext.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Thu Jun 09 20:22:22 2011 +0200
@@ -241,7 +241,7 @@
val rangeT = Term.range_type typ handle Match =>
err_in_mfix "Missing structure argument for indexed syntax" mfix;
- val xs = map Ast.Variable (Name.invents Name.context "xa" (length args - 1));
+ val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
val (xs1, xs2) = chop (find_index is_index args) xs;
val i = Ast.Variable "i";
val lhs = Ast.mk_appl (Ast.Constant indexed_const)
--- a/src/Pure/axclass.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/axclass.ML Thu Jun 09 20:22:22 2011 +0200
@@ -265,7 +265,7 @@
|> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
- val names = Name.invents Name.context Name.aT (length Ss);
+ val names = Name.invent Name.context Name.aT (length Ss);
val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names;
val completions = super_class_completions |> map (fn c1 =>
@@ -445,7 +445,7 @@
val (th', thy') = Global_Theory.store_thm
(Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
- val args = Name.names Name.context Name.aT Ss;
+ val args = Name.invent_names Name.context Name.aT Ss;
val T = Type (t, map TFree args);
val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
--- a/src/Pure/conjunction.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/conjunction.ML Thu Jun 09 20:22:22 2011 +0200
@@ -130,7 +130,7 @@
local
fun conjs thy n =
- let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
+ let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n)
in (As, mk_conjunction_balanced As) end;
val B = read_prop "B";
--- a/src/Pure/display.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/display.ML Thu Jun 09 20:22:22 2011 +0200
@@ -156,7 +156,7 @@
val tfrees = map (fn v => TFree (v, []));
fun pretty_type syn (t, (Type.LogicalType n)) =
if syn then NONE
- else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
+ else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
| pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) =
if syn <> syn' then NONE
else SOME (Pretty.block
--- a/src/Pure/logic.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/logic.ML Thu Jun 09 20:22:22 2011 +0200
@@ -253,7 +253,7 @@
fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
fun mk_arities (t, Ss, S) =
- let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
+ let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
in map (fn c => mk_of_class (T, c)) S end;
fun dest_arity tm =
@@ -279,7 +279,7 @@
val extra = fold (Sorts.remove_sort o #2) present shyps;
val n = length present;
- val (names1, names2) = Name.invents Name.context Name.aT (n + length extra) |> chop n;
+ val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
val present_map =
map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
--- a/src/Pure/more_thm.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/more_thm.ML Thu Jun 09 20:22:22 2011 +0200
@@ -341,7 +341,7 @@
fun stripped_sorts thy t =
let
val tfrees = rev (map TFree (Term.add_tfrees t []));
- val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
+ val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees));
val strip = tfrees ~~ tfrees';
val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
--- a/src/Pure/name.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/name.ML Thu Jun 09 20:22:22 2011 +0200
@@ -21,8 +21,8 @@
val make_context: string list -> context
val declare: string -> context -> context
val is_declared: context -> string -> bool
- val invents: context -> string -> int -> string list
- val names: context -> string -> 'a list -> (string * 'a) list
+ val invent: context -> string -> int -> string list
+ val invent_names: context -> string -> 'a list -> (string * 'a) list
val invent_list: string list -> string -> int -> string list
val variant: string -> context -> string * context
val variant_list: string list -> string list -> string list
@@ -94,21 +94,19 @@
fun make_context used = fold declare used context;
-(* invents *)
+(* invent names *)
-fun invents ctxt =
+fun invent ctxt =
let
fun invs _ 0 = []
| invs x n =
- let val x' = Symbol.bump_string x in
- if is_declared ctxt x then invs x' n
- else x :: invs x' (n - 1)
- end;
+ let val x' = Symbol.bump_string x
+ in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
in invs o clean end;
-fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
+fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
-val invent_list = invents o make_context;
+val invent_list = invent o make_context;
(* variants *)
--- a/src/Pure/proofterm.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/proofterm.ML Thu Jun 09 20:22:22 2011 +0200
@@ -952,7 +952,7 @@
fun canonical_instance typs =
let
- val names = Name.invents Name.context Name.aT (length typs);
+ val names = Name.invent Name.context Name.aT (length typs);
val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs;
in instantiate (instT, []) end;
--- a/src/Pure/term.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/term.ML Thu Jun 09 20:22:22 2011 +0200
@@ -957,7 +957,7 @@
else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
- let val [x] = Name.invents used Name.uu 1
+ let val [x] = Name.invent used Name.uu 1
in (Free (Name.internal x, T), Name.declare x used) end
| free_dummy_patterns (Abs (x, T, b)) used =
let val (b', used') = free_dummy_patterns b used
--- a/src/Pure/type_infer.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/type_infer.ML Thu Jun 09 20:22:22 2011 +0200
@@ -96,7 +96,7 @@
val used =
(fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
- val names = Name.invents used ("?" ^ Name.aT) (length parms);
+ val names = Name.invent used ("?" ^ Name.aT) (length parms);
val tab = Vartab.make (parms ~~ names);
fun finish_typ T =
@@ -117,7 +117,7 @@
fun subst_param (xi, S) (inst, used) =
if is_param xi then
let
- val [a] = Name.invents used Name.aT 1;
+ val [a] = Name.invent used Name.aT 1;
val used' = Name.declare a used;
in (((xi, S), TFree (a, S)) :: inst, used') end
else (inst, used);
--- a/src/Pure/variable.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/variable.ML Thu Jun 09 20:22:22 2011 +0200
@@ -391,7 +391,7 @@
fun invent_types Ss ctxt =
let
- val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss;
+ val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
in (tfrees, ctxt') end;
--- a/src/Tools/Code/code_scala.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Tools/Code/code_scala.ML Thu Jun 09 20:22:22 2011 +0200
@@ -149,7 +149,7 @@
fun print_def name (vs, ty) [] =
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
- val params = Name.invents (snd reserved) "a" (length tys);
+ val params = Name.invent (snd reserved) "a" (length tys);
val tyvars = intro_tyvars vs reserved;
val vars = intro_vars params reserved;
in
@@ -214,7 +214,7 @@
(fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
(applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
["final", "case", "class", deresolve co]) vs_args)
- (Name.names (snd reserved) "a" tys),
+ (Name.invent_names (snd reserved) "a" tys),
str "extends",
applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
((str o deresolve) name) vs
@@ -238,9 +238,9 @@
fun print_classparam_def (classparam, ty) =
let
val (tys, ty) = Code_Thingol.unfold_fun ty;
- val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
+ val [implicit_name] = Name.invent (snd reserved) (lookup_tyvar tyvars v) 1;
val proto_vars = intro_vars [implicit_name] reserved;
- val auxs = Name.invents (snd proto_vars) "a" (length tys);
+ val auxs = Name.invent (snd proto_vars) "a" (length tys);
val vars = intro_vars auxs proto_vars;
in
concat [str "def", constraint (Pretty.block [applify "(" ")"
@@ -267,7 +267,7 @@
val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
let
- val aux_tys = Name.names (snd reserved) "a" tys;
+ val aux_tys = Name.invent_names (snd reserved) "a" tys;
val auxs = map fst aux_tys;
val vars = intro_vars auxs reserved;
val aux_abstr = if null auxs then [] else [enum "," "(" ")"
--- a/src/Tools/Code/code_thingol.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Thu Jun 09 20:22:22 2011 +0200
@@ -237,7 +237,7 @@
| unfold_abs_eta tys t =
let
val ctxt = fold_varnames Name.declare t Name.context;
- val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
+ val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
fun eta_expand k (c as (name, (_, tys)), ts) =
@@ -248,7 +248,7 @@
then error ("Impossible eta-expansion for constant " ^ quote name) else ();
val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
val vs_tys = (map o apfst) SOME
- (Name.names ctxt "a" ((take l o drop j) tys));
+ (Name.invent_names ctxt "a" ((take l o drop j) tys));
in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
fun contains_dict_var t =
@@ -671,7 +671,7 @@
val classparams = these_classparams class;
val further_classparams = maps these_classparams
((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
- val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
+ val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
@@ -820,7 +820,7 @@
val k = length ts;
val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
- val vs = Name.names ctxt "a" tys;
+ val vs = Name.invent_names ctxt "a" tys;
in
fold_map (translate_typ thy algbr eqngr permissive) tys
##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
--- a/src/Tools/nbe.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Tools/nbe.ML Thu Jun 09 20:22:22 2011 +0200
@@ -330,7 +330,8 @@
val vs = (fold o Code_Thingol.fold_varnames)
(fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
val names = Name.make_context (map fst vs);
- fun declare v k ctxt = let val vs = Name.invents ctxt v k
+ fun declare v k ctxt =
+ let val vs = Name.invent ctxt v k
in (vs, fold Name.declare vs ctxt) end;
val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
then declare v (k - 1) #>> (fn vs => (v, vs))
@@ -372,7 +373,7 @@
fun assemble_eqns (c, (num_args, (dicts, eqns))) =
let
val default_args = map nbe_default
- (Name.invents Name.context "a" (num_args - length dicts));
+ (Name.invent Name.context "a" (num_args - length dicts));
val eqns' = map_index (assemble_eqn c dicts default_args) eqns
@ (if c = "" then [] else [(nbe_fun (length eqns) c,
[([ml_list (rev (dicts @ default_args))],
@@ -421,7 +422,7 @@
| eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
let
val names = map snd super_classes @ map fst classparams;
- val params = Name.invents Name.context "d" (length names);
+ val params = Name.invent Name.context "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
[([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],