--- a/src/HOL/HOLCF/Tools/cont_consts.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Fri Nov 29 17:40:15 2024 +0100
@@ -40,7 +40,7 @@
val c = Sign.full_name thy b
val c1 = Lexicon.mark_syntax c
val c2 = Lexicon.mark_const c
- val xs = Name.invent Name.context "xa" (Mixfix.mixfix_args thy_ctxt mx)
+ val xs = Name.invent_global "xa" (Mixfix.mixfix_args thy_ctxt mx)
val trans_rules =
Syntax.Parse_Print_Rule
(Ast.mk_appl (Ast.Constant c1) (map Ast.Variable xs),
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Nov 29 17:40:15 2024 +0100
@@ -50,7 +50,7 @@
fun check_size_type thy T_name size_name =
let
val n = Sign.arity_number thy T_name;
- val As = map (fn s => TFree (s, \<^sort>\<open>type\<close>)) (Name.invent Name.context Name.aT n);
+ val As = map (fn s => TFree (s, \<^sort>\<open>type\<close>)) (Name.invent_global_types n);
val T = Type (T_name, As);
val size_T = map mk_to_natT As ---> mk_to_natT T;
val size_const = Const (size_name, size_T);
--- a/src/HOL/Tools/Function/fun.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/Function/fun.ML Fri Nov 29 17:40:15 2024 +0100
@@ -67,7 +67,7 @@
val (argTs, rT) = chop n (binder_types fT)
|> apsnd (fn Ts => Ts ---> body_type fT)
- val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
+ val qs = map Free (Name.invent_global "a" n ~~ argTs)
in
HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
Const (\<^const_name>\<open>undefined\<close>, rT))
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Nov 29 17:40:15 2024 +0100
@@ -643,7 +643,7 @@
map (fn xs => nth xs m) raw_vss
|> foldr1 (Sorts.inter_sort (Sign.classes_of thy));
val sorts = map inter_sort ms;
- val vs = Name.invent_names Name.context Name.aT sorts;
+ val vs = Name.invent_types_global sorts;
fun norm_constr (raw_vs, (c, T)) =
(c, map_atyps
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Nov 29 17:40:15 2024 +0100
@@ -72,7 +72,7 @@
fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
let
- val frees = map Free (Name.invent_names Name.context "a" (map (K \<^typ>\<open>narrowing_term\<close>) tys))
+ val frees = map Free (Name.invent_names_global "a" (map (K \<^typ>\<open>narrowing_term\<close>) tys))
val narrowing_term =
\<^term>\<open>Quickcheck_Narrowing.Narrowing_constructor\<close> $ HOLogic.mk_number \<^typ>\<open>integer\<close> i $
HOLogic.mk_list \<^typ>\<open>narrowing_term\<close> (rev frees)
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Nov 29 17:40:15 2024 +0100
@@ -219,7 +219,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.invent_names Name.context "x" (map snd simple_tTs);
+ val vs = Name.invent_names_global "x" (map snd simple_tTs);
val tc = HOLogic.mk_return T \<^typ>\<open>Random.seed\<close>
(HOLogic.mk_valtermify_app c vs simpleT);
val t = HOLogic.mk_ST
--- a/src/HOL/Tools/code_evaluation.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Fri Nov 29 17:40:15 2024 +0100
@@ -60,8 +60,7 @@
fun mk_term_of_eq thy ty (c, (_, tys)) =
let
- val t = list_comb (Const (c, tys ---> ty),
- map Free (Name.invent_names Name.context "a" tys));
+ val t = list_comb (Const (c, tys ---> ty), map Free (Name.invent_names_global "a" tys));
val (arg, rhs) =
apply2 (Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
(t,
--- a/src/HOL/Tools/record.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Tools/record.ML Fri Nov 29 17:40:15 2024 +0100
@@ -1719,7 +1719,7 @@
fun termifyT T = HOLogic.mk_prodT (T, \<^typ>\<open>unit \<Rightarrow> term\<close>);
val T = Type (tyco, map TFree vs);
val Tm = termifyT T;
- val params = Name.invent_names Name.context "x" Ts;
+ val params = Name.invent_names_global "x" Ts;
val lhs = HOLogic.mk_random T size;
val tc = HOLogic.mk_return Tm \<^typ>\<open>Random.seed\<close>
(HOLogic.mk_valtermify_app extN params T);
@@ -1739,7 +1739,7 @@
fun termifyT T = HOLogic.mk_prodT (T, \<^typ>\<open>unit \<Rightarrow> term\<close>);
val T = Type (tyco, map TFree vs);
val test_function = Free ("f", termifyT T --> \<^typ>\<open>(bool \<times> term list) option\<close>);
- val params = Name.invent_names Name.context "x" Ts;
+ val params = Name.invent_names_global "x" Ts;
fun mk_full_exhaustive U = \<^Const>\<open>full_exhaustive_class.full_exhaustive U\<close>;
val lhs = mk_full_exhaustive T $ test_function $ size;
val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
--- a/src/HOL/Typerep.thy Fri Nov 29 11:26:17 2024 +0100
+++ b/src/HOL/Typerep.thy Fri Nov 29 17:40:15 2024 +0100
@@ -48,7 +48,7 @@
fun add_typerep tyco thy =
let
val sorts = replicate (Sign.arity_number thy tyco) \<^sort>\<open>typerep\<close>;
- val vs = Name.invent_names Name.context "'a" sorts;
+ val vs = Name.invent_types_global sorts;
val ty = Type (tyco, map TFree vs);
val lhs = \<^Const>\<open>typerep ty\<close> $ Free ("T", Term.itselfT ty);
val rhs = \<^Const>\<open>Typerep\<close> $ HOLogic.mk_literal tyco
--- a/src/Pure/Build/export_theory.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/Build/export_theory.ML Fri Nov 29 17:40:15 2024 +0100
@@ -224,7 +224,7 @@
(fn c =>
(fn Type.Logical_Type n =>
SOME (fn () =>
- encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
+ encode_type (get_syntax_type thy_ctxt c, Name.invent_global_types n, NONE))
| Type.Abbreviation (args, U, false) =>
SOME (fn () =>
encode_type (get_syntax_type thy_ctxt c, args, SOME U))
--- a/src/Pure/Isar/class.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/Isar/class.ML Fri Nov 29 17:40:15 2024 +0100
@@ -276,7 +276,7 @@
let
val vs = strip_abs_vars t;
val vts = map snd vs
- |> Name.invent_names Name.context Name.uu
+ |> Name.invent_names_global Name.uu
|> map (fn (v, T) => Var ((v, 0), T));
in (betapplys (t, vts), betapplys (Const c_ty, vts)) end;
@@ -581,7 +581,7 @@
(raw_tyco, raw_sorts, raw_sort)) raw_tycos;
val tycos = map #1 all_arities;
val (_, sorts, sort) = hd all_arities;
- val vs = Name.invent_names Name.context Name.aT sorts;
+ val vs = Name.invent_types_global sorts;
in (tycos, vs, sort) end;
--- a/src/Pure/Isar/code.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/Isar/code.ML Fri Nov 29 17:40:15 2024 +0100
@@ -114,7 +114,7 @@
fun devarify ty =
let
val tys = build (fold_atyps (fn TVar vi_sort => AList.update (op =) vi_sort) ty);
- val vs = Name.invent Name.context Name.aT (length tys);
+ val vs = Name.invent_global_types (length tys);
val mapping = map2 (fn v => fn (vi, sort) => (vi, TFree (v, sort))) vs tys;
in Term.typ_subst_TVars mapping ty end;
@@ -544,7 +544,7 @@
of [tyco] => tyco
| [] => error "Empty constructor set"
| tycos => error ("Different type constructors in constructor set: " ^ commas_quote tycos)
- val vs = Name.invent Name.context Name.aT (Sign.arity_number thy tyco);
+ val vs = Name.invent_global_types (Sign.arity_number thy tyco);
fun inst vs' (c, (vs, ty)) =
let
val the_v = the o AList.lookup (op =) (vs ~~ vs');
@@ -562,7 +562,7 @@
fun get_type thy tyco = case lookup_vs_type_spec thy tyco
of SOME (vs, type_spec) => apfst (pair vs) (constructors_of type_spec)
| NONE => Sign.arity_number thy tyco
- |> Name.invent Name.context Name.aT
+ |> Name.invent_global_types
|> map (rpair [])
|> rpair []
|> rpair false;
@@ -962,7 +962,7 @@
val inter_sorts =
build o fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd);
val sorts = map_transpose inter_sorts vss;
- val vts = Name.invent_names Name.context Name.aT sorts;
+ val vts = Name.invent_types_global sorts;
fun instantiate vs =
Thm.instantiate (TVars.make (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts), Vars.empty);
val thms' = map2 instantiate vss thms;
--- a/src/Pure/Isar/proof_display.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/Isar/proof_display.ML Fri Nov 29 17:40:15 2024 +0100
@@ -56,7 +56,7 @@
val tfrees = map (fn v => TFree (v, []));
fun pretty_type syn (t, Type.Logical_Type n) =
if syn then NONE
- else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
+ else SOME (prt_typ (Type (t, tfrees (Name.invent_global_types n))))
| pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
if syn <> syn' then NONE
else SOME (Pretty.block
--- a/src/Pure/Isar/typedecl.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/Isar/typedecl.ML Fri Nov 29 17:40:15 2024 +0100
@@ -60,7 +60,7 @@
fun final_type (b, n) lthy =
let
val c = Local_Theory.full_name lthy b;
- val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+ val args = map (fn a => TFree (a, [])) (Name.invent_global_types n);
in
Local_Theory.background_theory
(Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy
--- a/src/Pure/Syntax/syntax_ext.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Nov 29 17:40:15 2024 +0100
@@ -388,7 +388,7 @@
val rangeT = Term.range_type typ handle Match =>
err_in_mixfix "Missing structure argument for indexed syntax";
- val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
+ val xs = map Ast.Variable (Name.invent_global "xa" (length args - 1));
val (xs1, xs2) = chop (find_index is_index args) xs;
val i = Ast.Variable "i";
val lhs =
--- a/src/Pure/axclass.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/axclass.ML Fri Nov 29 17:40:15 2024 +0100
@@ -280,7 +280,7 @@
val binding =
Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
- val args = Name.invent_names Name.context Name.aT Ss;
+ val args = Name.invent_types_global Ss;
val missing_params =
Sign.complete_sort thy [c]
|> maps (these o Option.map #params o try (get_info thy))
--- a/src/Pure/conjunction.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/conjunction.ML Fri Nov 29 17:40:15 2024 +0100
@@ -144,7 +144,7 @@
let
val As =
map (fn A => Thm.global_cterm_of bootstrap_thy (Free (A, propT)))
- (Name.invent Name.context "" n);
+ (Name.invent_global "" n);
in (As, mk_conjunction_balanced As) end;
val B = read_prop "B";
--- a/src/Pure/logic.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/logic.ML Fri Nov 29 17:40:15 2024 +0100
@@ -335,7 +335,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.invent Name.context Name.aT (length Ss), Ss))
+ let val T = Type (t, ListPair.map TFree (Name.invent_global_types (length Ss), Ss))
in map (fn c => mk_of_class (T, c)) S end;
fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c]));
@@ -375,7 +375,7 @@
val {present, extra} = present_sorts shyps present_set;
val n = Types.size present_set;
- val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
+ val (names1, names2) = Name.invent_global_types (n + length extra) |> chop n;
val present_map =
map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
--- a/src/Pure/name.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/name.ML Fri Nov 29 17:40:15 2024 +0100
@@ -29,7 +29,11 @@
val declare_renamed: string * string -> context -> context
val is_declared: context -> string -> bool
val invent: context -> string -> int -> string list
+ val invent_global: string -> int -> string list
+ val invent_global_types: int -> string list
val invent_names: context -> string -> 'a list -> (string * 'a) list
+ val invent_names_global: string -> 'a list -> (string * 'a) list
+ val invent_types_global: 'a list -> (string * 'a) list
val invent_list: string list -> string -> int -> string list
val variant: string -> context -> string * context
val variant_bound: string -> context -> string * context
@@ -126,7 +130,12 @@
in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
in invs o clean end;
+val invent_global = invent context;
+val invent_global_types = invent_global aT;
+
fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
+fun invent_names_global x xs = invent_names context x xs;
+fun invent_types_global xs = invent_names context aT xs;
val invent_list = invent o make_context;
--- a/src/Pure/theory.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/theory.ML Fri Nov 29 17:40:15 2024 +0100
@@ -287,7 +287,7 @@
fun add_deps_type c thy =
let
val n = Sign.arity_number thy c;
- val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+ val args = map (fn a => TFree (a, [])) (Name.invent_global_types n);
in thy |> add_deps_global "" (type_dep (c, args)) [] end
fun specify_const decl thy =
--- a/src/Pure/thm.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/thm.ML Fri Nov 29 17:40:15 2024 +0100
@@ -2609,7 +2609,7 @@
let
val thy = theory_of_thm thm;
val tvars = build_rev (Term.add_tvars (prop_of thm));
- val names = Name.invent Name.context Name.aT (length tvars);
+ val names = Name.invent_global_types (length tvars);
val tinst =
map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names;
in instantiate (TVars.make tinst, Vars.empty) thm end
--- a/src/Tools/Code/code_preproc.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Tools/Code/code_preproc.ML Fri Nov 29 17:40:15 2024 +0100
@@ -202,7 +202,7 @@
val t = Thm.term_of ct;
val vs_original =
build (fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t);
- val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
+ val vs_normalized = Name.invent_types_global (map snd vs_original);
val normalize =
map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
val normalization =
--- a/src/Tools/Code/code_thingol.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Tools/Code/code_thingol.ML Fri Nov 29 17:40:15 2024 +0100
@@ -656,7 +656,7 @@
val class_params = these_class_params class;
val superclass_params = maps these_class_params
((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
- val vs = Name.invent_names Name.context Name.aT (Sorts.mg_domain algebra tyco [class]);
+ val vs = Name.invent_types_global (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';
--- a/src/Tools/nbe.ML Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Tools/nbe.ML Fri Nov 29 17:40:15 2024 +0100
@@ -381,8 +381,7 @@
fun assemble_eqns (sym, (num_args, (dicts, eqns))) =
let
- val default_args = map nbe_default
- (Name.invent Name.context "a" (num_args - length dicts));
+ val default_args = map nbe_default (Name.invent_global "a" (num_args - length dicts));
val eqns' = map_index (assemble_eqn sym dicts default_args) eqns
@ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym,
[([ml_list (rev (dicts @ default_args))],
@@ -436,7 +435,7 @@
| eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) =
let
val syms = map Class_Relation classrels @ map (Constant o fst) classparams;
- val params = Name.invent Name.context "d" (length syms);
+ val params = Name.invent_global "d" (length syms);
fun mk (k, sym) =
(sym, ([(v, [])],
[([dummy_const sym_class [] `$$ map (IVar o SOME) params],