# HG changeset patch # User wenzelm # Date 1732898415 -3600 # Node ID 08574da77b4ae60de7708320ef50a96697e2b5d2 # Parent f76a5849b570e8b9469c4360a3ec09a5be43d462 clarified signature: shorten common cases; diff -r f76a5849b570 -r 08574da77b4a src/HOL/HOLCF/Tools/cont_consts.ML --- 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), diff -r f76a5849b570 -r 08574da77b4a src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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>\type\)) (Name.invent Name.context Name.aT n); + val As = map (fn s => TFree (s, \<^sort>\type\)) (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); diff -r f76a5849b570 -r 08574da77b4a src/HOL/Tools/Function/fun.ML --- 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>\undefined\, rT)) diff -r f76a5849b570 -r 08574da77b4a src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- 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 diff -r f76a5849b570 -r 08574da77b4a src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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>\narrowing_term\) tys)) + val frees = map Free (Name.invent_names_global "a" (map (K \<^typ>\narrowing_term\) tys)) val narrowing_term = \<^term>\Quickcheck_Narrowing.Narrowing_constructor\ $ HOLogic.mk_number \<^typ>\integer\ i $ HOLogic.mk_list \<^typ>\narrowing_term\ (rev frees) diff -r f76a5849b570 -r 08574da77b4a src/HOL/Tools/Quickcheck/random_generators.ML --- 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>\Random.seed\ (HOLogic.mk_valtermify_app c vs simpleT); val t = HOLogic.mk_ST diff -r f76a5849b570 -r 08574da77b4a src/HOL/Tools/code_evaluation.ML --- 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, diff -r f76a5849b570 -r 08574da77b4a src/HOL/Tools/record.ML --- 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>\unit \ term\); 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>\Random.seed\ (HOLogic.mk_valtermify_app extN params T); @@ -1739,7 +1739,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>\(bool \ term list) option\); - val params = Name.invent_names Name.context "x" Ts; + val params = Name.invent_names_global "x" Ts; fun mk_full_exhaustive U = \<^Const>\full_exhaustive_class.full_exhaustive U\; val lhs = mk_full_exhaustive T $ test_function $ size; val tc = test_function $ (HOLogic.mk_valtermify_app extN params T); diff -r f76a5849b570 -r 08574da77b4a src/HOL/Typerep.thy --- 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>\typerep\; - 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>\typerep ty\ $ Free ("T", Term.itselfT ty); val rhs = \<^Const>\Typerep\ $ HOLogic.mk_literal tyco diff -r f76a5849b570 -r 08574da77b4a src/Pure/Build/export_theory.ML --- 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)) diff -r f76a5849b570 -r 08574da77b4a src/Pure/Isar/class.ML --- 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; diff -r f76a5849b570 -r 08574da77b4a src/Pure/Isar/code.ML --- 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; diff -r f76a5849b570 -r 08574da77b4a src/Pure/Isar/proof_display.ML --- 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 diff -r f76a5849b570 -r 08574da77b4a src/Pure/Isar/typedecl.ML --- 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 diff -r f76a5849b570 -r 08574da77b4a src/Pure/Syntax/syntax_ext.ML --- 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 = diff -r f76a5849b570 -r 08574da77b4a src/Pure/axclass.ML --- 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)) diff -r f76a5849b570 -r 08574da77b4a src/Pure/conjunction.ML --- 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"; diff -r f76a5849b570 -r 08574da77b4a src/Pure/logic.ML --- 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; diff -r f76a5849b570 -r 08574da77b4a src/Pure/name.ML --- 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; diff -r f76a5849b570 -r 08574da77b4a src/Pure/theory.ML --- 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 = diff -r f76a5849b570 -r 08574da77b4a src/Pure/thm.ML --- 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 diff -r f76a5849b570 -r 08574da77b4a src/Tools/Code/code_preproc.ML --- 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 = diff -r f76a5849b570 -r 08574da77b4a src/Tools/Code/code_thingol.ML --- 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'; diff -r f76a5849b570 -r 08574da77b4a src/Tools/nbe.ML --- 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],