# HG changeset patch # User wenzelm # Date 1307643742 -7200 # Node ID 84472e1985152189d8edfa5d0b85d67d1eb972db # Parent 10d731b06ed7761165e258d789598494bd6bd027 tuned signature: Name.invent and Name.invent_names; diff -r 10d731b06ed7 -r 84472e198515 doc-src/IsarImplementation/Thy/Prelim.thy --- 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 = diff -r 10d731b06ed7 -r 84472e198515 doc-src/IsarImplementation/Thy/document/Prelim.tex --- 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{}% diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Boogie/Tools/boogie_loader.ML --- 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) diff -r 10d731b06ed7 -r 84472e198515 src/HOL/HOLCF/Tools/cont_consts.ML --- 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 diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Tools/Datatype/datatype_data.ML --- 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); diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Tools/Function/fun.ML --- 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)) diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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 = diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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) diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Tools/Quickcheck/random_generators.ML --- 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 diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Tools/code_evaluation.ML --- 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) diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Tools/enriched_type.ML --- 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; diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Tools/record.ML --- 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 = diff -r 10d731b06ed7 -r 84472e198515 src/HOL/Typerep.thy --- 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); diff -r 10d731b06ed7 -r 84472e198515 src/Provers/Arith/fast_lin_arith.ML --- 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 diff -r 10d731b06ed7 -r 84472e198515 src/Pure/Isar/class.ML --- 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; diff -r 10d731b06ed7 -r 84472e198515 src/Pure/Isar/code.ML --- 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')))); diff -r 10d731b06ed7 -r 84472e198515 src/Pure/Isar/specification.ML --- 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) diff -r 10d731b06ed7 -r 84472e198515 src/Pure/Proof/proof_rewrite_rules.ML --- 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; diff -r 10d731b06ed7 -r 84472e198515 src/Pure/Syntax/syntax_ext.ML --- 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) diff -r 10d731b06ed7 -r 84472e198515 src/Pure/axclass.ML --- 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; diff -r 10d731b06ed7 -r 84472e198515 src/Pure/conjunction.ML --- 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"; diff -r 10d731b06ed7 -r 84472e198515 src/Pure/display.ML --- 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 diff -r 10d731b06ed7 -r 84472e198515 src/Pure/logic.ML --- 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; diff -r 10d731b06ed7 -r 84472e198515 src/Pure/more_thm.ML --- 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; diff -r 10d731b06ed7 -r 84472e198515 src/Pure/name.ML --- 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 *) diff -r 10d731b06ed7 -r 84472e198515 src/Pure/proofterm.ML --- 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; diff -r 10d731b06ed7 -r 84472e198515 src/Pure/term.ML --- 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 diff -r 10d731b06ed7 -r 84472e198515 src/Pure/type_infer.ML --- 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); diff -r 10d731b06ed7 -r 84472e198515 src/Pure/variable.ML --- 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; diff -r 10d731b06ed7 -r 84472e198515 src/Tools/Code/code_scala.ML --- 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 "," "(" ")" diff -r 10d731b06ed7 -r 84472e198515 src/Tools/Code/code_thingol.ML --- 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) diff -r 10d731b06ed7 -r 84472e198515 src/Tools/nbe.ML --- 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],