tuned signature: Name.invent and Name.invent_names;
authorwenzelm
Thu Jun 09 20:22:22 2011 +0200 (2011-06-09)
changeset 4332984472e198515
parent 43328 10d731b06ed7
child 43330 c6bbeca3ee06
tuned signature: Name.invent and Name.invent_names;
doc-src/IsarImplementation/Thy/Prelim.thy
doc-src/IsarImplementation/Thy/document/Prelim.tex
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/HOLCF/Tools/cont_consts.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/enriched_type.ML
src/HOL/Tools/record.ML
src/HOL/Typerep.thy
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/axclass.ML
src/Pure/conjunction.ML
src/Pure/display.ML
src/Pure/logic.ML
src/Pure/more_thm.ML
src/Pure/name.ML
src/Pure/proofterm.ML
src/Pure/term.ML
src/Pure/type_infer.ML
src/Pure/variable.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Wed Jun 08 22:16:21 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Thu Jun 09 20:22:22 2011 +0200
     1.3 @@ -854,7 +854,7 @@
     1.4    @{index_ML_type Name.context} \\
     1.5    @{index_ML Name.context: Name.context} \\
     1.6    @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
     1.7 -  @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
     1.8 +  @{index_ML Name.invent: "Name.context -> string -> int -> string list"} \\
     1.9    @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\
    1.10    \end{mldecls}
    1.11    \begin{mldecls}
    1.12 @@ -875,7 +875,7 @@
    1.13    \item @{ML Name.declare}~@{text "name"} enters a used name into the
    1.14    context.
    1.15  
    1.16 -  \item @{ML Name.invents}~@{text "context name n"} produces @{text
    1.17 +  \item @{ML Name.invent}~@{text "context name n"} produces @{text
    1.18    "n"} fresh names derived from @{text "name"}.
    1.19  
    1.20    \item @{ML Name.variant}~@{text "name context"} produces a fresh
    1.21 @@ -897,7 +897,7 @@
    1.22    fresh names from the initial @{ML Name.context}. *}
    1.23  
    1.24  ML {*
    1.25 -  val list1 = Name.invents Name.context "a" 5;
    1.26 +  val list1 = Name.invent Name.context "a" 5;
    1.27    @{assert} (list1 = ["a", "b", "c", "d", "e"]);
    1.28  
    1.29    val list2 =
    1.30 @@ -914,7 +914,7 @@
    1.31  ML {*
    1.32    val names = Variable.names_of @{context};
    1.33  
    1.34 -  val list1 = Name.invents names "a" 5;
    1.35 +  val list1 = Name.invent names "a" 5;
    1.36    @{assert} (list1 = ["d", "e", "f", "g", "h"]);
    1.37  
    1.38    val list2 =
     2.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Wed Jun 08 22:16:21 2011 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Jun 09 20:22:22 2011 +0200
     2.3 @@ -1254,7 +1254,7 @@
     2.4    \indexdef{}{ML type}{Name.context}\verb|type Name.context| \\
     2.5    \indexdef{}{ML}{Name.context}\verb|Name.context: Name.context| \\
     2.6    \indexdef{}{ML}{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
     2.7 -  \indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
     2.8 +  \indexdef{}{ML}{Name.invent}\verb|Name.invent: Name.context -> string -> int -> string list| \\
     2.9    \indexdef{}{ML}{Name.variant}\verb|Name.variant: string -> Name.context -> string * Name.context| \\
    2.10    \end{mldecls}
    2.11    \begin{mldecls}
    2.12 @@ -1275,7 +1275,7 @@
    2.13    \item \verb|Name.declare|~\isa{name} enters a used name into the
    2.14    context.
    2.15  
    2.16 -  \item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
    2.17 +  \item \verb|Name.invent|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
    2.18  
    2.19    \item \verb|Name.variant|~\isa{name\ context} produces a fresh
    2.20    variant of \isa{name}; the result is declared to the context.
    2.21 @@ -1325,7 +1325,7 @@
    2.22  \isatagML
    2.23  \isacommand{ML}\isamarkupfalse%
    2.24  \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
    2.25 -\ \ 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
    2.26 +\ \ 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
    2.27  \ \ %
    2.28  \isaantiq
    2.29  assert{}%
    2.30 @@ -1370,7 +1370,7 @@
    2.31  \endisaantiq
    2.32  {\isaliteral{3B}{\isacharsemicolon}}\isanewline
    2.33  \isanewline
    2.34 -\ \ 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
    2.35 +\ \ 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
    2.36  \ \ %
    2.37  \isaantiq
    2.38  assert{}%
     3.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Wed Jun 08 22:16:21 2011 +0200
     3.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Jun 09 20:22:22 2011 +0200
     3.3 @@ -86,7 +86,7 @@
     3.4          SOME type_name => (((name, type_name), log_ex name type_name), thy)
     3.5        | NONE =>
     3.6            let
     3.7 -            val args = map (rpair dummyS) (Name.invents Name.context "'a" arity)
     3.8 +            val args = map (rpair dummyS) (Name.invent Name.context "'a" arity)
     3.9              val (T, thy') =
    3.10                Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
    3.11              val type_name = fst (Term.dest_Type T)
     4.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Wed Jun 08 22:16:21 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Thu Jun 09 20:22:22 2011 +0200
     4.3 @@ -23,7 +23,7 @@
     4.4  
     4.5  fun trans_rules name2 name1 n mx =
     4.6    let
     4.7 -    val vnames = Name.invents Name.context "a" n
     4.8 +    val vnames = Name.invent Name.context "a" n
     4.9      val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
    4.10    in
    4.11      [Syntax.Parse_Print_Rule
     5.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Jun 08 22:16:21 2011 +0200
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jun 09 20:22:22 2011 +0200
     5.3 @@ -407,7 +407,7 @@
     5.4      fun inter_sort m = map (fn xs => nth xs m) raw_vss
     5.5        |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
     5.6      val sorts = map inter_sort ms;
     5.7 -    val vs = Name.names Name.context Name.aT sorts;
     5.8 +    val vs = Name.invent_names Name.context Name.aT sorts;
     5.9  
    5.10      fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
    5.11        (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
     6.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Jun 08 22:16:21 2011 +0200
     6.2 +++ b/src/HOL/Tools/Function/fun.ML	Thu Jun 09 20:22:22 2011 +0200
     6.3 @@ -64,7 +64,7 @@
     6.4          val (argTs, rT) = chop n (binder_types fT)
     6.5            |> apsnd (fn Ts => Ts ---> body_type fT)
     6.6  
     6.7 -        val qs = map Free (Name.invents Name.context "a" n ~~ argTs)
     6.8 +        val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
     6.9        in
    6.10          HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    6.11            Const ("HOL.undefined", rT))
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Jun 08 22:16:21 2011 +0200
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jun 09 20:22:22 2011 +0200
     7.3 @@ -129,7 +129,7 @@
     7.4  
     7.5  fun declare_names s xs ctxt =
     7.6    let
     7.7 -    val res = Name.names ctxt s xs
     7.8 +    val res = Name.invent_names ctxt s xs
     7.9    in (res, fold Name.declare (map fst res) ctxt) end
    7.10    
    7.11  fun split_all_pairs thy th =
     8.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jun 08 22:16:21 2011 +0200
     8.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 20:22:22 2011 +0200
     8.3 @@ -67,7 +67,7 @@
     8.4  
     8.5  fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
     8.6    let
     8.7 -    val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys))
     8.8 +    val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
     8.9      val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
    8.10        $ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
    8.11      val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
     9.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Jun 08 22:16:21 2011 +0200
     9.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Jun 09 20:22:22 2011 +0200
     9.3 @@ -214,7 +214,7 @@
     9.4          val tTs = (map o apsnd) termifyT simple_tTs;
     9.5          val is_rec = exists is_some ks;
     9.6          val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
     9.7 -        val vs = Name.names Name.context "x" (map snd simple_tTs);
     9.8 +        val vs = Name.invent_names Name.context "x" (map snd simple_tTs);
     9.9          val tc = HOLogic.mk_return T @{typ Random.seed}
    9.10            (HOLogic.mk_valtermify_app c vs simpleT);
    9.11          val t = HOLogic.mk_ST
    10.1 --- a/src/HOL/Tools/code_evaluation.ML	Wed Jun 08 22:16:21 2011 +0200
    10.2 +++ b/src/HOL/Tools/code_evaluation.ML	Thu Jun 09 20:22:22 2011 +0200
    10.3 @@ -57,7 +57,7 @@
    10.4  fun mk_term_of_eq thy ty (c, (_, tys)) =
    10.5    let
    10.6      val t = list_comb (Const (c, tys ---> ty),
    10.7 -      map Free (Name.names Name.context "a" tys));
    10.8 +      map Free (Name.invent_names Name.context "a" tys));
    10.9      val (arg, rhs) =
   10.10        pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
   10.11          (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
    11.1 --- a/src/HOL/Tools/enriched_type.ML	Wed Jun 08 22:16:21 2011 +0200
    11.2 +++ b/src/HOL/Tools/enriched_type.ML	Thu Jun 09 20:22:22 2011 +0200
    11.3 @@ -98,7 +98,7 @@
    11.4      val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
    11.5      fun invents n k nctxt =
    11.6        let
    11.7 -        val names = Name.invents nctxt n k;
    11.8 +        val names = Name.invent nctxt n k;
    11.9        in (names, fold Name.declare names nctxt) end;
   11.10      val ((names21, names32), nctxt) = Variable.names_of ctxt
   11.11        |> invents "f" (length Ts21)
   11.12 @@ -120,7 +120,7 @@
   11.13      val mapper31 = mk_mapper T3 T1 args31;
   11.14      val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   11.15        (HOLogic.mk_comp (mapper21, mapper32), mapper31);
   11.16 -    val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3)
   11.17 +    val x = Free (the_single (Name.invent nctxt (Long_Name.base_name tyco) 1), T3)
   11.18      val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   11.19        (mapper21 $ (mapper32 $ x), mapper31 $ x);
   11.20      val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
    12.1 --- a/src/HOL/Tools/record.ML	Wed Jun 08 22:16:21 2011 +0200
    12.2 +++ b/src/HOL/Tools/record.ML	Thu Jun 09 20:22:22 2011 +0200
    12.3 @@ -1801,7 +1801,7 @@
    12.4      fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
    12.5      val T = Type (tyco, map TFree vs);
    12.6      val Tm = termifyT T;
    12.7 -    val params = Name.names Name.context "x" Ts;
    12.8 +    val params = Name.invent_names Name.context "x" Ts;
    12.9      val lhs = HOLogic.mk_random T size;
   12.10      val tc = HOLogic.mk_return Tm @{typ Random.seed}
   12.11        (HOLogic.mk_valtermify_app extN params T);
   12.12 @@ -1820,7 +1820,7 @@
   12.13      fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
   12.14      val T = Type (tyco, map TFree vs);
   12.15      val test_function = Free ("f", termifyT T --> @{typ "term list option"});
   12.16 -    val params = Name.names Name.context "x" Ts;
   12.17 +    val params = Name.invent_names Name.context "x" Ts;
   12.18      fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   12.19        --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
   12.20      fun mk_full_exhaustive T =
    13.1 --- a/src/HOL/Typerep.thy	Wed Jun 08 22:16:21 2011 +0200
    13.2 +++ b/src/HOL/Typerep.thy	Thu Jun 09 20:22:22 2011 +0200
    13.3 @@ -47,7 +47,7 @@
    13.4  fun add_typerep tyco thy =
    13.5    let
    13.6      val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
    13.7 -    val vs = Name.names Name.context "'a" sorts;
    13.8 +    val vs = Name.invent_names Name.context "'a" sorts;
    13.9      val ty = Type (tyco, map TFree vs);
   13.10      val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
   13.11        $ Free ("T", Term.itselfT ty);
    14.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jun 08 22:16:21 2011 +0200
    14.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jun 09 20:22:22 2011 +0200
    14.3 @@ -749,7 +749,7 @@
    14.4                      let
    14.5                        val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params)
    14.6                        val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes
    14.7 -                        (Name.invents (Variable.names_of ctxt') Name.uu (length Ts - length params))
    14.8 +                        (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params))
    14.9                        val params' = (more_names @ param_names) ~~ Ts
   14.10                      in
   14.11                        trace_ex ctxt'' params' atoms (discr initems) n hist
    15.1 --- a/src/Pure/Isar/class.ML	Wed Jun 08 22:16:21 2011 +0200
    15.2 +++ b/src/Pure/Isar/class.ML	Thu Jun 09 20:22:22 2011 +0200
    15.3 @@ -426,7 +426,7 @@
    15.4        (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    15.5      val tycos = map #1 all_arities;
    15.6      val (_, sorts, sort) = hd all_arities;
    15.7 -    val vs = Name.names Name.context Name.aT sorts;
    15.8 +    val vs = Name.invent_names Name.context Name.aT sorts;
    15.9    in (tycos, vs, sort) end;
   15.10  
   15.11  
    16.1 --- a/src/Pure/Isar/code.ML	Wed Jun 08 22:16:21 2011 +0200
    16.2 +++ b/src/Pure/Isar/code.ML	Thu Jun 09 20:22:22 2011 +0200
    16.3 @@ -433,7 +433,7 @@
    16.4        in (c, (vs'', binder_types ty')) end;
    16.5      val c' :: cs' = map (analyze_constructor thy) cs;
    16.6      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
    16.7 -    val vs = Name.names Name.context Name.aT sorts;
    16.8 +    val vs = Name.invent_names Name.context Name.aT sorts;
    16.9      val cs''' = map (inst vs) cs'';
   16.10    in (tyco, (vs, rev cs''')) end;
   16.11  
   16.12 @@ -444,7 +444,7 @@
   16.13  fun get_type thy tyco = case get_type_entry thy tyco
   16.14   of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
   16.15    | NONE => arity_number thy tyco
   16.16 -      |> Name.invents Name.context Name.aT
   16.17 +      |> Name.invent Name.context Name.aT
   16.18        |> map (rpair [])
   16.19        |> rpair []
   16.20        |> rpair false;
   16.21 @@ -779,7 +779,7 @@
   16.22          fun inter_sorts vs =
   16.23            fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
   16.24          val sorts = map_transpose inter_sorts vss;
   16.25 -        val vts = Name.names Name.context Name.aT sorts;
   16.26 +        val vts = Name.invent_names Name.context Name.aT sorts;
   16.27          val thms' =
   16.28            map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
   16.29          val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
    17.1 --- a/src/Pure/Isar/specification.ML	Wed Jun 08 22:16:21 2011 +0200
    17.2 +++ b/src/Pure/Isar/specification.ML	Thu Jun 09 20:22:22 2011 +0200
    17.3 @@ -93,7 +93,7 @@
    17.4        (case duplicates (op =) commons of [] => ()
    17.5        | dups => error ("Duplicate local variables " ^ commas_quote dups));
    17.6      val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
    17.7 -    val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
    17.8 +    val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
    17.9      val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
   17.10  
   17.11      fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
    18.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jun 08 22:16:21 2011 +0200
    18.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jun 09 20:22:22 2011 +0200
    18.3 @@ -200,7 +200,7 @@
    18.4      fun rew_term Ts t =
    18.5        let
    18.6          val frees =
    18.7 -          map Free (Name.invents (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
    18.8 +          map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
    18.9          val t' = r (subst_bounds (frees, t));
   18.10          fun strip [] t = t
   18.11            | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
    19.1 --- a/src/Pure/Syntax/syntax_ext.ML	Wed Jun 08 22:16:21 2011 +0200
    19.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 20:22:22 2011 +0200
    19.3 @@ -241,7 +241,7 @@
    19.4            val rangeT = Term.range_type typ handle Match =>
    19.5              err_in_mfix "Missing structure argument for indexed syntax" mfix;
    19.6  
    19.7 -          val xs = map Ast.Variable (Name.invents Name.context "xa" (length args - 1));
    19.8 +          val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
    19.9            val (xs1, xs2) = chop (find_index is_index args) xs;
   19.10            val i = Ast.Variable "i";
   19.11            val lhs = Ast.mk_appl (Ast.Constant indexed_const)
    20.1 --- a/src/Pure/axclass.ML	Wed Jun 08 22:16:21 2011 +0200
    20.2 +++ b/src/Pure/axclass.ML	Thu Jun 09 20:22:22 2011 +0200
    20.3 @@ -265,7 +265,7 @@
    20.4        |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) =>
    20.5              c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
    20.6  
    20.7 -    val names = Name.invents Name.context Name.aT (length Ss);
    20.8 +    val names = Name.invent Name.context Name.aT (length Ss);
    20.9      val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names;
   20.10  
   20.11      val completions = super_class_completions |> map (fn c1 =>
   20.12 @@ -445,7 +445,7 @@
   20.13      val (th', thy') = Global_Theory.store_thm
   20.14        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
   20.15  
   20.16 -    val args = Name.names Name.context Name.aT Ss;
   20.17 +    val args = Name.invent_names Name.context Name.aT Ss;
   20.18      val T = Type (t, map TFree args);
   20.19      val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
   20.20  
    21.1 --- a/src/Pure/conjunction.ML	Wed Jun 08 22:16:21 2011 +0200
    21.2 +++ b/src/Pure/conjunction.ML	Thu Jun 09 20:22:22 2011 +0200
    21.3 @@ -130,7 +130,7 @@
    21.4  local
    21.5  
    21.6  fun conjs thy n =
    21.7 -  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invents Name.context "A" n)
    21.8 +  let val As = map (fn A => Thm.cterm_of thy (Free (A, propT))) (Name.invent Name.context "A" n)
    21.9    in (As, mk_conjunction_balanced As) end;
   21.10  
   21.11  val B = read_prop "B";
    22.1 --- a/src/Pure/display.ML	Wed Jun 08 22:16:21 2011 +0200
    22.2 +++ b/src/Pure/display.ML	Thu Jun 09 20:22:22 2011 +0200
    22.3 @@ -156,7 +156,7 @@
    22.4      val tfrees = map (fn v => TFree (v, []));
    22.5      fun pretty_type syn (t, (Type.LogicalType n)) =
    22.6            if syn then NONE
    22.7 -          else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
    22.8 +          else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
    22.9        | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) =
   22.10            if syn <> syn' then NONE
   22.11            else SOME (Pretty.block
    23.1 --- a/src/Pure/logic.ML	Wed Jun 08 22:16:21 2011 +0200
    23.2 +++ b/src/Pure/logic.ML	Thu Jun 09 20:22:22 2011 +0200
    23.3 @@ -253,7 +253,7 @@
    23.4  fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
    23.5  
    23.6  fun mk_arities (t, Ss, S) =
    23.7 -  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
    23.8 +  let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
    23.9    in map (fn c => mk_of_class (T, c)) S end;
   23.10  
   23.11  fun dest_arity tm =
   23.12 @@ -279,7 +279,7 @@
   23.13      val extra = fold (Sorts.remove_sort o #2) present shyps;
   23.14  
   23.15      val n = length present;
   23.16 -    val (names1, names2) = Name.invents Name.context Name.aT (n + length extra) |> chop n;
   23.17 +    val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
   23.18  
   23.19      val present_map =
   23.20        map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
    24.1 --- a/src/Pure/more_thm.ML	Wed Jun 08 22:16:21 2011 +0200
    24.2 +++ b/src/Pure/more_thm.ML	Thu Jun 09 20:22:22 2011 +0200
    24.3 @@ -341,7 +341,7 @@
    24.4  fun stripped_sorts thy t =
    24.5    let
    24.6      val tfrees = rev (map TFree (Term.add_tfrees t []));
    24.7 -    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
    24.8 +    val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees));
    24.9      val strip = tfrees ~~ tfrees';
   24.10      val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
   24.11      val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
    25.1 --- a/src/Pure/name.ML	Wed Jun 08 22:16:21 2011 +0200
    25.2 +++ b/src/Pure/name.ML	Thu Jun 09 20:22:22 2011 +0200
    25.3 @@ -21,8 +21,8 @@
    25.4    val make_context: string list -> context
    25.5    val declare: string -> context -> context
    25.6    val is_declared: context -> string -> bool
    25.7 -  val invents: context -> string -> int -> string list
    25.8 -  val names: context -> string -> 'a list -> (string * 'a) list
    25.9 +  val invent: context -> string -> int -> string list
   25.10 +  val invent_names: context -> string -> 'a list -> (string * 'a) list
   25.11    val invent_list: string list -> string -> int -> string list
   25.12    val variant: string -> context -> string * context
   25.13    val variant_list: string list -> string list -> string list
   25.14 @@ -94,21 +94,19 @@
   25.15  fun make_context used = fold declare used context;
   25.16  
   25.17  
   25.18 -(* invents *)
   25.19 +(* invent names *)
   25.20  
   25.21 -fun invents ctxt =
   25.22 +fun invent ctxt =
   25.23    let
   25.24      fun invs _ 0 = []
   25.25        | invs x n =
   25.26 -          let val x' = Symbol.bump_string x in
   25.27 -            if is_declared ctxt x then invs x' n
   25.28 -            else x :: invs x' (n - 1)
   25.29 -          end;
   25.30 +          let val x' = Symbol.bump_string x
   25.31 +          in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
   25.32    in invs o clean end;
   25.33  
   25.34 -fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
   25.35 +fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
   25.36  
   25.37 -val invent_list = invents o make_context;
   25.38 +val invent_list = invent o make_context;
   25.39  
   25.40  
   25.41  (* variants *)
    26.1 --- a/src/Pure/proofterm.ML	Wed Jun 08 22:16:21 2011 +0200
    26.2 +++ b/src/Pure/proofterm.ML	Thu Jun 09 20:22:22 2011 +0200
    26.3 @@ -952,7 +952,7 @@
    26.4  
    26.5  fun canonical_instance typs =
    26.6    let
    26.7 -    val names = Name.invents Name.context Name.aT (length typs);
    26.8 +    val names = Name.invent Name.context Name.aT (length typs);
    26.9      val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs;
   26.10    in instantiate (instT, []) end;
   26.11  
    27.1 --- a/src/Pure/term.ML	Wed Jun 08 22:16:21 2011 +0200
    27.2 +++ b/src/Pure/term.ML	Thu Jun 09 20:22:22 2011 +0200
    27.3 @@ -957,7 +957,7 @@
    27.4    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
    27.5  
    27.6  fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
    27.7 -      let val [x] = Name.invents used Name.uu 1
    27.8 +      let val [x] = Name.invent used Name.uu 1
    27.9        in (Free (Name.internal x, T), Name.declare x used) end
   27.10    | free_dummy_patterns (Abs (x, T, b)) used =
   27.11        let val (b', used') = free_dummy_patterns b used
    28.1 --- a/src/Pure/type_infer.ML	Wed Jun 08 22:16:21 2011 +0200
    28.2 +++ b/src/Pure/type_infer.ML	Thu Jun 09 20:22:22 2011 +0200
    28.3 @@ -96,7 +96,7 @@
    28.4      val used =
    28.5        (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt));
    28.6      val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
    28.7 -    val names = Name.invents used ("?" ^ Name.aT) (length parms);
    28.8 +    val names = Name.invent used ("?" ^ Name.aT) (length parms);
    28.9      val tab = Vartab.make (parms ~~ names);
   28.10  
   28.11      fun finish_typ T =
   28.12 @@ -117,7 +117,7 @@
   28.13      fun subst_param (xi, S) (inst, used) =
   28.14        if is_param xi then
   28.15          let
   28.16 -          val [a] = Name.invents used Name.aT 1;
   28.17 +          val [a] = Name.invent used Name.aT 1;
   28.18            val used' = Name.declare a used;
   28.19          in (((xi, S), TFree (a, S)) :: inst, used') end
   28.20        else (inst, used);
    29.1 --- a/src/Pure/variable.ML	Wed Jun 08 22:16:21 2011 +0200
    29.2 +++ b/src/Pure/variable.ML	Thu Jun 09 20:22:22 2011 +0200
    29.3 @@ -391,7 +391,7 @@
    29.4  
    29.5  fun invent_types Ss ctxt =
    29.6    let
    29.7 -    val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss;
    29.8 +    val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss;
    29.9      val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   29.10    in (tfrees, ctxt') end;
   29.11  
    30.1 --- a/src/Tools/Code/code_scala.ML	Wed Jun 08 22:16:21 2011 +0200
    30.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jun 09 20:22:22 2011 +0200
    30.3 @@ -149,7 +149,7 @@
    30.4      fun print_def name (vs, ty) [] =
    30.5            let
    30.6              val (tys, ty') = Code_Thingol.unfold_fun ty;
    30.7 -            val params = Name.invents (snd reserved) "a" (length tys);
    30.8 +            val params = Name.invent (snd reserved) "a" (length tys);
    30.9              val tyvars = intro_tyvars vs reserved;
   30.10              val vars = intro_vars params reserved;
   30.11            in
   30.12 @@ -214,7 +214,7 @@
   30.13                      (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
   30.14                      (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
   30.15                        ["final", "case", "class", deresolve co]) vs_args)
   30.16 -                    (Name.names (snd reserved) "a" tys),
   30.17 +                    (Name.invent_names (snd reserved) "a" tys),
   30.18                      str "extends",
   30.19                      applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
   30.20                        ((str o deresolve) name) vs
   30.21 @@ -238,9 +238,9 @@
   30.22              fun print_classparam_def (classparam, ty) =
   30.23                let
   30.24                  val (tys, ty) = Code_Thingol.unfold_fun ty;
   30.25 -                val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
   30.26 +                val [implicit_name] = Name.invent (snd reserved) (lookup_tyvar tyvars v) 1;
   30.27                  val proto_vars = intro_vars [implicit_name] reserved;
   30.28 -                val auxs = Name.invents (snd proto_vars) "a" (length tys);
   30.29 +                val auxs = Name.invent (snd proto_vars) "a" (length tys);
   30.30                  val vars = intro_vars auxs proto_vars;
   30.31                in
   30.32                  concat [str "def", constraint (Pretty.block [applify "(" ")"
   30.33 @@ -267,7 +267,7 @@
   30.34              val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
   30.35              fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
   30.36                let
   30.37 -                val aux_tys = Name.names (snd reserved) "a" tys;
   30.38 +                val aux_tys = Name.invent_names (snd reserved) "a" tys;
   30.39                  val auxs = map fst aux_tys;
   30.40                  val vars = intro_vars auxs reserved;
   30.41                  val aux_abstr = if null auxs then [] else [enum "," "(" ")"
    31.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jun 08 22:16:21 2011 +0200
    31.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jun 09 20:22:22 2011 +0200
    31.3 @@ -237,7 +237,7 @@
    31.4    | unfold_abs_eta tys t =
    31.5        let
    31.6          val ctxt = fold_varnames Name.declare t Name.context;
    31.7 -        val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
    31.8 +        val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
    31.9        in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
   31.10  
   31.11  fun eta_expand k (c as (name, (_, tys)), ts) =
   31.12 @@ -248,7 +248,7 @@
   31.13        then error ("Impossible eta-expansion for constant " ^ quote name) else ();
   31.14      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
   31.15      val vs_tys = (map o apfst) SOME
   31.16 -      (Name.names ctxt "a" ((take l o drop j) tys));
   31.17 +      (Name.invent_names ctxt "a" ((take l o drop j) tys));
   31.18    in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
   31.19  
   31.20  fun contains_dict_var t =
   31.21 @@ -671,7 +671,7 @@
   31.22      val classparams = these_classparams class;
   31.23      val further_classparams = maps these_classparams
   31.24        ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
   31.25 -    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
   31.26 +    val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
   31.27      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
   31.28      val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
   31.29        Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
   31.30 @@ -820,7 +820,7 @@
   31.31        val k = length ts;
   31.32        val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
   31.33        val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
   31.34 -      val vs = Name.names ctxt "a" tys;
   31.35 +      val vs = Name.invent_names ctxt "a" tys;
   31.36      in
   31.37        fold_map (translate_typ thy algbr eqngr permissive) tys
   31.38        ##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs)
    32.1 --- a/src/Tools/nbe.ML	Wed Jun 08 22:16:21 2011 +0200
    32.2 +++ b/src/Tools/nbe.ML	Thu Jun 09 20:22:22 2011 +0200
    32.3 @@ -330,7 +330,8 @@
    32.4          val vs = (fold o Code_Thingol.fold_varnames)
    32.5            (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
    32.6          val names = Name.make_context (map fst vs);
    32.7 -        fun declare v k ctxt = let val vs = Name.invents ctxt v k
    32.8 +        fun declare v k ctxt =
    32.9 +          let val vs = Name.invent ctxt v k
   32.10            in (vs, fold Name.declare vs ctxt) end;
   32.11          val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
   32.12            then declare v (k - 1) #>> (fn vs => (v, vs))
   32.13 @@ -372,7 +373,7 @@
   32.14      fun assemble_eqns (c, (num_args, (dicts, eqns))) =
   32.15        let
   32.16          val default_args = map nbe_default
   32.17 -          (Name.invents Name.context "a" (num_args - length dicts));
   32.18 +          (Name.invent Name.context "a" (num_args - length dicts));
   32.19          val eqns' = map_index (assemble_eqn c dicts default_args) eqns
   32.20            @ (if c = "" then [] else [(nbe_fun (length eqns) c,
   32.21              [([ml_list (rev (dicts @ default_args))],
   32.22 @@ -421,7 +422,7 @@
   32.23    | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
   32.24        let
   32.25          val names = map snd super_classes @ map fst classparams;
   32.26 -        val params = Name.invents Name.context "d" (length names);
   32.27 +        val params = Name.invent Name.context "d" (length names);
   32.28          fun mk (k, name) =
   32.29            (name, ([(v, [])],
   32.30              [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],