# HG changeset patch # User wenzelm # Date 1733005836 -3600 # Node ID 878bc24681d90ae6f92b01a4262d53b846fb6266 # Parent ed766dfdd2f1b55b0ebfc520fd362bf08ef432b9# Parent cdc43c0fdbfc299d7333304d9d79c619a9798c7b merged diff -r ed766dfdd2f1 -r 878bc24681d9 NEWS --- a/NEWS Fri Nov 29 10:35:47 2024 +0100 +++ b/NEWS Sat Nov 30 23:30:36 2024 +0100 @@ -81,12 +81,12 @@ * Command "unbundle b" and its variants like "context includes b" allow an optional name prefix with the reserved word "no": "unbundle no b" -etc. This inverts the polarity of bundled declarations like 'notation' -vs. 'no_notation', and thus avoids redundant bundle definitions like -"foobar_syntax" vs. "no_foobar_syntax", because "no foobar_syntax" may -be used instead. Consequently, the syntax for multiple bundle names has -been changed slightly, demanding an explicit 'and' keyword. Minor -INCOMPATIBILITY. +etc. This reverses both the order and polarity of bundled declarations +like 'notation' vs. 'no_notation', and thus avoids redundant bundle +definitions like "foobar_syntax" vs. "no_foobar_syntax", because "no +foobar_syntax" may be used instead. Consequently, the syntax for +multiple bundle names has been changed slightly, demanding an explicit +'and' keyword. Minor INCOMPATIBILITY. * Command "open_bundle b" is like "bundle b" followed by "unbundle b", so its declarations are applied immediately, but also named for later diff -r ed766dfdd2f1 -r 878bc24681d9 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Sat Nov 30 23:30:36 2024 +0100 @@ -297,7 +297,9 @@ \<^item> @{command type_notation} versus @{command no_type_notation} This also works recursively for the @{command unbundle} command as - declaration inside a @{command bundle} definition. + declaration inside a @{command bundle} definition: \<^verbatim>\no\ means that + both the order and polarity of declarations is reversed (following + algebraic group laws). Here is an artificial example of bundling various configuration options: diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Data_Structures/Define_Time_Function.ML --- a/src/HOL/Data_Structures/Define_Time_Function.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Data_Structures/Define_Time_Function.ML Sat Nov 30 23:30:36 2024 +0100 @@ -883,7 +883,7 @@ | args _ = [] val dom_vars = terms |> hd |> get_l |> map_types (map_atyps freeTypes) - |> args |> Variable.variant_frees lthy [] + |> args |> Variable.variant_names lthy val dom_args = List.foldl (fn (t,p) => HOLogic.mk_prod ((Free t),p)) (Free (hd dom_vars)) (tl dom_vars) diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Hoare/hoare_tac.ML Sat Nov 30 23:30:36 2024 +0100 @@ -87,7 +87,7 @@ fun Mset ctxt prop = let - val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())]; + val [(Mset, _), (P, _)] = Variable.variant_names ctxt [("Mset", ()), ("P", ())]; val vars = get_vars prop; val varsT = fastype_of (mk_bodyC vars); diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Inductive.thy Sat Nov 30 23:30:36 2024 +0100 @@ -532,7 +532,7 @@ let fun fun_tr ctxt [cs] = let - val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context))); + val x = Syntax.free (#1 (Name.variant "x" (Name.build_context (Term.declare_free_names cs)))); val ft = Case_Translation.case_tr true ctxt [x, cs]; in lambda x ft end in [(\<^syntax_const>\_lam_pats_syntax\, fun_tr)] end diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Library/refute.ML Sat Nov 30 23:30:36 2024 +0100 @@ -1186,8 +1186,8 @@ (a, T) :: strip_all_vars t | strip_all_vars _ = [] : (string * typ) list val strip_t = strip_all_body ex_closure - val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure) - val subst_t = Term.subst_bounds (map Free frees, strip_t) + val frees = Term.variant_frees strip_t (strip_all_vars ex_closure) + val subst_t = Term.subst_bounds (map Free (rev frees), strip_t) in find_model ctxt (actual_params ctxt params) assm_ts subst_t true end; diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Nov 30 23:30:36 2024 +0100 @@ -245,9 +245,9 @@ if null (preds_of ps prem) then prem else lift_prem prem) prems, HOLogic.mk_Trueprop (lift_pred p ts)); - val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params') + val vs = map (Var o apfst (rpair 0)) (Term.variant_frees prem params') in - (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem))) + (Logic.list_all (params', prem), (vs, subst_bounds (rev vs, prem))) end) prems); val ind_vars = diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Nov 30 23:30:36 2024 +0100 @@ -146,8 +146,8 @@ in Option.map prove (map_term f prop (the_default prop opt)) end; fun abs_params params t = - let val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term t params) - in (Logic.list_all (params, t), (rev vs, subst_bounds (vs, t))) end; + let val vs = map (Var o apfst (rpair 0)) (Term.variant_frees t params) + in (Logic.list_all (params, t), (vs, subst_bounds (rev vs, t))) end; fun inst_params thy (vs, p) th cts = let val env = Pattern.first_order_match thy (p, Thm.prop_of th) diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Sat Nov 30 23:30:36 2024 +0100 @@ -156,8 +156,7 @@ let val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); val rargs = map fst recs; - val subs = map (rpair dummyT o fst) - (rev (Term.rename_wrt_term rhs rargs)); + val subs = map (rpair dummyT o fst) (Term.variant_frees rhs rargs); val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => (Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss') handle RecError s => primrec_eq_err lthy s eq diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Nov 30 23:30:36 2024 +0100 @@ -274,11 +274,11 @@ in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end (* This assumes that distinct names are mapped to distinct names by - "Variable.variant_frees". This does not hold in general but should hold for + "Variable.variant_names". This does not hold in general but should hold for ATP-generated Skolem function names, since these end with a digit and "variant_frees" appends letters. *) fun desymbolize_and_fresh_up ctxt s = - fst (hd (Variable.variant_frees ctxt [] [(Name.desymbolize (SOME false) s, ())])) + fst (singleton (Variable.variant_names ctxt) (Name.desymbolize (SOME false) s, ())) (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas are typed. The code is similar to "term_of_atp_fo". *) diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Sat Nov 30 23:30:36 2024 +0100 @@ -410,7 +410,7 @@ let val (t, (frees, params)) = Logic.goal_params (Thm.prop_of goal) i - ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free)) + ||> (map dest_Free #> Variable.variant_names ctxt #> `(map Free)) val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees in (rev params, hyp_ts, concl_t) end diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Nov 30 23:30:36 2024 +0100 @@ -262,7 +262,7 @@ |> mk_TFrees' (map Type.sort_of_atyp As0); val fpT = Type (fpT_name, As); - val (var_name, ()) = singleton (Variable.variant_frees ctxt []) ("x", ()); + val (var_name, ()) = singleton (Variable.variant_names ctxt) ("x", ()); val var = Free (var_name, fpT); val goal = mk_Trueprop_eq (expand_to_ctr_term ctxt fpT var, var); @@ -394,7 +394,7 @@ val fun_T = fastype_of fun_t; val num_args = num_binder_types fun_T; - val f = Free (singleton (Variable.variant_frees ctxt []) ("f", fun_T)); + val f = Free (singleton (Variable.variant_names ctxt) ("f", fun_T)); val is_self_call = curry (op aconv) fun_t; val has_self_call = exists_subterm is_self_call; @@ -777,7 +777,8 @@ val (arg_Ts, _) = strip_type (fastype_of fun_t); val added_Ts = drop (length arg_ts) arg_Ts; val free_names = mk_names (length added_Ts) "x" ~~ added_Ts; - val free_args = Variable.variant_frees ctxt [rhs, lhs] free_names |> map Free; + val free_args = + Variable.variant_names (fold Variable.declare_names [rhs, lhs] ctxt) free_names |> map Free; in (arg_ts @ free_args, list_comb (rhs, free_args)) end; @@ -1315,8 +1316,8 @@ else (c, d) :: (add_association a b r); fun new_TVar known_TVars = - Name.invent_list (map (fst o fst o dest_TVar) known_TVars) "x" 1 - |> (fn [s] => TVar ((s, 0), [])); + let val [a] = Name.invent_list (map (fst o fst o dest_TVar) known_TVars) Name.aT 1 + in TVar ((a, 0), []) end fun instantiate_type inferred_types = Term.typ_subst_TVars (map (apfst (fst o dest_TVar)) inferred_types); diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Nov 30 23:30:36 2024 +0100 @@ -1212,7 +1212,9 @@ (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss''); val ps = - Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)]; + Variable.variant_names + (fold Variable.declare_names (maps (maps #fun_args) disc_eqnss) lthy) + [("P", HOLogic.boolT)]; val exhaust_thmss = map2 (fn false => K [] diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sat Nov 30 23:30:36 2024 +0100 @@ -394,7 +394,8 @@ if member (op =) frees t then Free (the_single (Term.variant_frees t [dest_Free t])) else t; val args = replicate n_args ("", dummyT) - |> Term.rename_wrt_term t + |> Term.variant_frees t + |> rev |> map Free |> fold (fn (ctr_arg_idx, (arg_idx, _)) => nth_map arg_idx (K (nth ctr_args ctr_arg_idx))) diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Sat Nov 30 23:30:36 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 a => TFree (a, \<^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 ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sat Nov 30 23:30:36 2024 +0100 @@ -161,7 +161,7 @@ | replace_dummies t used = (t, used); fun dest_case1 (t as Const (\<^syntax_const>\_case1\, _) $ l $ r) = - let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context) in + let val (l', _) = replace_dummies l (Name.build_context (Term.declare_free_names t)) in abs_pat l' [] (Syntax.const \<^const_syntax>\case_elem\ $ Term_Position.strip_positions l' $ r) end @@ -198,7 +198,7 @@ fun mk_clauses (Const (\<^const_syntax>\case_nil\, _)) = [] | mk_clauses (Const (\<^const_syntax>\case_cons\, _) $ t $ u) = - mk_clause t [] (Term.declare_term_frees t Name.context) :: mk_clauses u + mk_clause t [] (Name.build_context (Term.declare_free_names t)) :: mk_clauses u | mk_clauses _ = raise Match; in list_comb (Syntax.const \<^syntax_const>\_case_syntax\ $ x $ @@ -248,7 +248,7 @@ completion.*) fun add_row_used ((prfx, pats), (tm, _)) = - fold Term.declare_term_frees (tm :: pats @ map Free prfx); + fold Term.declare_free_names (tm :: pats @ map Free prfx); (*try to preserve names given by user*) fun default_name "" (Free (name', _)) = name' @@ -307,7 +307,7 @@ val (xs, _) = fold_map Name.variant (replicate (length ps) "x") - (fold Term.declare_term_frees gvars used'); + (fold Term.declare_free_names gvars used'); in [((prfx, gvars @ map Free (xs ~~ Ts)), (Const (\<^const_name>\undefined\, res_ty), ~1))] @@ -361,7 +361,7 @@ | SOME (case_comb, constructors) => let val pty = body_type cT; - val used' = fold Term.declare_term_frees us used; + val used' = fold Term.declare_free_names us used; val nrows = maps (expand constructors used' pty) rows; val subproblems = partition used' constructors pty range_ty nrows; val (pat_rect, dtrees) = @@ -440,8 +440,7 @@ fun decode_cases (Const (\<^const_name>\case_nil\, _)) = [] | decode_cases (Const (\<^const_name>\case_cons\, _) $ t $ u) = - decode_clause t [] (Term.declare_term_frees t Name.context) :: - decode_cases u + decode_clause t [] (Name.build_context (Term.declare_free_names t)) :: decode_cases u | decode_cases _ = case_error "decode_cases"; fun check_case ctxt = @@ -479,10 +478,7 @@ map (pair "x") (drop j (take i (binder_types (fastype_of t)))), []) else chop i zs; val u = fold_rev Term.abs ys (strip_abs_body t); - val xs' = map Free - ((fold_map Name.variant (map fst xs) - (Term.declare_term_names u used) |> fst) ~~ - map snd xs); + val xs' = map Free (Name.variant_names (Term.declare_term_names u used) xs); val (xs1, xs2) = chop j xs' in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end; fun is_dependent i t = @@ -562,7 +558,7 @@ | encode_case _ _ = case_error "encode_case"; fun strip_case' ctxt d (pat, rhs) = - (case dest_case ctxt d (Term.declare_term_frees pat Name.context) rhs of + (case dest_case ctxt d (Name.build_context (Term.declare_free_names pat)) rhs of SOME (exp as Free _, clauses) => if Term.exists_subterm (curry (op aconv) exp) pat andalso not (exists (fn (_, rhs') => diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Function/fun.ML Sat Nov 30 23:30:36 2024 +0100 @@ -66,8 +66,7 @@ val n = arity_of fname 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_names_global "a" argTs) in HOLogic.mk_eq(list_comb (Free (fname, fT), qs), Const (\<^const_name>\undefined\, rT)) diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Function/function_elims.ML --- a/src/HOL/Tools/Function/function_elims.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Function/function_elims.ML Sat Nov 30 23:30:36 2024 +0100 @@ -79,7 +79,7 @@ val n_fs = length fs; fun variant_free used_term v = - Free (singleton (Variable.variant_frees ctxt [used_term]) v); + Free (singleton (Variable.variant_names (Variable.declare_names used_term ctxt)) v); fun mk_partial_elim_rule (idx, f) = let diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat Nov 30 23:30:36 2024 +0100 @@ -121,7 +121,8 @@ val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] - val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) + val (Pbool :: xs') = + map Free (Variable.variant_names (fold Variable.declare_names allqnames ctxt) (("P", HOLogic.boolT) :: xs)) val Cs' = map (Pattern.rewrite_term (Proof_Context.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Sat Nov 30 23:30:36 2024 +0100 @@ -247,7 +247,7 @@ fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs = Ts, ...}) = let val [P, x] = - Variable.variant_frees ctxt [] [("P", \<^typ>\bool\), ("x", HOLogic.mk_tupleT Ts)] + Variable.variant_names ctxt [("P", \<^typ>\bool\), ("x", HOLogic.mk_tupleT Ts)] |> map (Thm.cterm_of ctxt o Free); val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x)); diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Function/pattern_split.ML --- a/src/HOL/Tools/Function/pattern_split.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Function/pattern_split.ML Sat Nov 30 23:30:36 2024 +0100 @@ -20,7 +20,7 @@ fun new_var ctxt vs T = let - val [v] = Variable.variant_frees ctxt vs [("v", T)] + val v = singleton (Variable.variant_names (fold Variable.declare_names vs ctxt)) ("v", T) in (Free v :: vs, Free v) end diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Old_Datatype/old_primrec.ML --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Sat Nov 30 23:30:36 2024 +0100 @@ -149,8 +149,7 @@ let val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); val rargs = map fst recs; - val subs = map (rpair dummyT o fst) - (rev (Term.rename_wrt_term rhs rargs)); + val subs = map (rpair dummyT o fst) (Term.variant_frees rhs rargs); val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => (Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss') handle PrimrecError (s, NONE) => primrec_error_eqn s eq diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sat Nov 30 23:30:36 2024 +0100 @@ -642,8 +642,7 @@ fun inter_sort m = 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 (map inter_sort ms); fun norm_constr (raw_vs, (c, T)) = (c, map_atyps diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Nov 30 23:30:36 2024 +0100 @@ -991,8 +991,9 @@ mk_set_compr (t :: in_insert) ts xs else let - val uu as (uuN, uuT) = - singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t) + val uuT = fastype_of t + val uu as (uuN, _) = + singleton (Variable.variant_names (Variable.declare_names t ctxt')) ("uu", uuT) val set_compr = HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t)) diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Nov 30 23:30:36 2024 +0100 @@ -1204,7 +1204,7 @@ fun define_quickcheck_predicate t thy = let val (vs, t') = strip_abs t - val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *) + val vs' = Variable.variant_names (Proof_Context.init_global thy) vs (* FIXME proper context!? *) val t'' = subst_bounds (map Free (rev vs'), t') val (prems, concl) = strip_horn t'' val constname = "quickcheck" diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Nov 30 23:30:36 2024 +0100 @@ -127,26 +127,22 @@ val i = length (binder_types (fastype_of f)) - length args in funpow i (fn th => th RS meta_fun_cong) th end; -fun declare_names s xs ctxt = - let - val res = Name.invent_names ctxt s xs - in (res, fold Name.declare (map fst res) ctxt) end - fun split_all_pairs thy th = let val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val ((_, [th']), _) = Variable.import true [th] ctxt val t = Thm.prop_of th' val frees = Term.add_frees t [] - val freenames = Term.add_free_names t [] - val nctxt = Name.make_context freenames fun mk_tuple_rewrites (x, T) nctxt = let val Ts = HOLogic.flatten_tupleT T - val (xTs, nctxt') = declare_names x Ts nctxt + val xTs = Name.invent_names nctxt x Ts + val nctxt' = fold (Name.declare o #1) xTs nctxt val paths = HOLogic.flat_tupleT_paths T in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end - val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt + val (rewr, _) = + Name.build_context (Term.declare_free_names t) + |> fold_map mk_tuple_rewrites frees val t' = Pattern.rewrite_term thy rewr [] t val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Nov 30 23:30:36 2024 +0100 @@ -279,14 +279,12 @@ let val (constr, args) = strip_comb t val T = fastype_of t + val ctxt1 = fold Variable.declare_names (concl :: assms) ctxt val vars = - map Free - (Variable.variant_frees ctxt (concl :: assms) - (map (fn t => ("x", fastype_of t)) args)) + map Free (Variable.variant_names ctxt1 (map (fn t => ("x", fastype_of t)) args)) val varnames = map (fst o dest_Free) vars - val dummy_var = - Free (singleton - (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T)) + val ctxt2 = fold Variable.declare_names vars ctxt1 + val dummy_var = Free (singleton (Variable.variant_names ctxt2) ("dummy", T)) val new_assms = map HOLogic.mk_eq (vars ~~ args) val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars) val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Nov 30 23:30:36 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 (fn a => Free (a, \<^typ>\narrowing_term\)) (Name.invent_global "a" (length 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 ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Nov 30 23:30:36 2024 +0100 @@ -248,7 +248,7 @@ @{thm bot_fun_def}, @{thm less_bool_def}]) val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t) val (vs, body) = strip_all t' - val vs' = Variable.variant_frees ctxt [t'] vs + val vs' = Variable.variant_names (Variable.declare_names t' ctxt) vs in subst_bounds (map Free (rev vs'), body) end diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Nov 30 23:30:36 2024 +0100 @@ -33,7 +33,7 @@ let val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] - |> Variable.variant_frees lthy [rel] + |> Variable.variant_names (Variable.declare_names rel lthy) |> map Free in HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $ diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Nov 30 23:30:36 2024 +0100 @@ -139,8 +139,8 @@ (cf. "~~/src/Pure/Isar/obtain.ML") *) let val frees = map Free xs - val thesis = - Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT)) + val ctxt' = fold Variable.declare_names frees ctxt + val thesis = Free (singleton (Variable.variant_names ctxt') ("thesis", HOLogic.boolT)) val thesis_prop = HOLogic.mk_Trueprop thesis (* !!x1...xn. t ==> thesis *) diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/code_evaluation.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/functor.ML --- a/src/HOL/Tools/functor.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/functor.ML Sat Nov 30 23:30:36 2024 +0100 @@ -98,13 +98,9 @@ (if co then [false] else []) @ (if contra then [true] else [])) variances; val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances); val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances); - fun invents n k nctxt = - let - 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) - ||>> invents "f" (length Ts32); + |> Name.invent' "f" (length Ts21) + ||>> Name.invent' "f" (length Ts32); val T1 = Type (tyco, Ts1); val T2 = Type (tyco, Ts2); val T3 = Type (tyco, Ts3); diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/inductive.ML Sat Nov 30 23:30:36 2024 +0100 @@ -925,12 +925,12 @@ val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT; val fp_const = if coind then \<^Const>\gfp predT\ else \<^Const>\lfp predT\; + val ctxt1 = fold Variable.declare_names intr_ts lthy val p :: xs = - map Free (Variable.variant_frees lthy intr_ts + map Free (Variable.variant_names ctxt1 (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); - val bs = - map Free (Variable.variant_frees lthy (p :: xs @ intr_ts) - (map (rpair HOLogic.boolT) (mk_names "b" k))); + val ctxt2 = fold Variable.declare_names (p :: xs) ctxt1 + val bs = map Free (Variable.variant_names ctxt2 (map (rpair HOLogic.boolT) (mk_names "b" k))); fun subst t = (case dest_predicate cs params t of @@ -1001,8 +1001,8 @@ map_index (fn (i, ((b, mx), c)) => let val Ts = arg_types_of (length params) c; - val xs = - map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts)); + val ctxt = fold Variable.declare_names intr_ts lthy'; + val xs = map Free (Variable.variant_names ctxt (mk_names "x" (length Ts) ~~ Ts)); in ((b, mx), ((Thm.make_def_binding internals b, []), fold_rev lambda (params @ xs) diff -r ed766dfdd2f1 -r 878bc24681d9 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Tools/record.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Fri Nov 29 10:35:47 2024 +0100 +++ b/src/HOL/Typerep.thy Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Provers/preorder.ML --- a/src/Provers/preorder.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Provers/preorder.ML Sat Nov 30 23:30:36 2024 +0100 @@ -555,7 +555,7 @@ fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st => let val thy = Proof_Context.theory_of ctxt; - val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); + val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A))); val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); val C = subst_bounds (rfrees, Logic.strip_assums_concl A); val lesss = flat (map_index (mkasm_trans thy o swap) Hs); @@ -578,7 +578,7 @@ fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st => let val thy = Proof_Context.theory_of ctxt - val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); + val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A))); val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); val C = subst_bounds (rfrees, Logic.strip_assums_concl A); val lesss = flat (map_index (mkasm_quasi thy o swap) Hs); diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/Build/export_theory.ML --- a/src/Pure/Build/export_theory.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Build/export_theory.ML Sat Nov 30 23:30:36 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)) @@ -263,7 +263,7 @@ val args' = args |> filter (is_free o #1); val typargs' = typargs |> filter (is_free o #1); val used_typargs = fold (Name.declare o #1) typargs' used; - val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps; + val sorts = Name.invent_types used_typargs extra_shyps; in ((sorts @ typargs', args', prop), proof) end; fun standard_prop_of thm = @@ -390,7 +390,7 @@ (fn loc => fn () => SOME (fn () => let val {typargs, args, axioms} = locale_content thy loc; - val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context; + val used = Name.build_context (fold Name.declare (map #1 typargs @ map (#1 o #1) args)); in encode_locale used (typargs, args, axioms) end handle ERROR msg => cat_error msg ("The error(s) above occurred in locale " ^ diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Isar/bundle.ML Sat Nov 30 23:30:36 2024 +0100 @@ -126,10 +126,11 @@ val notes = if loc then Local_Theory.notes else Attrib.local_notes ""; val add0 = Syntax.get_polarity ctxt; val add1 = Syntax.effective_polarity ctxt add; + val bundle' = if add1 then bundle else rev (map (apsnd rev) bundle); in ctxt |> Context_Position.set_visible false - |> notes [(Binding.empty_atts, polarity_decls add1 @ bundle @ polarity_decls add0)] |> snd + |> notes [(Binding.empty_atts, polarity_decls add1 @ bundle' @ polarity_decls add0)] |> snd |> Context_Position.restore_visible ctxt end; diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Isar/class.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Isar/code.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Isar/object_logic.ML Sat Nov 30 23:30:36 2024 +0100 @@ -159,7 +159,7 @@ fun is_propositional ctxt T = T = propT orelse - let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T)) + let val x = Free (singleton (Variable.variant_names ctxt) ("x", T)) in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end; diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Isar/proof_display.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Isar/typedecl.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Proof/proof_checker.ML Sat Nov 30 23:30:36 2024 +0100 @@ -76,7 +76,7 @@ fn prf => let val prf_names = - Name.build_context (prf |> Proofterm.fold_proof_terms Term.declare_term_frees); + Name.build_context (prf |> Proofterm.fold_proof_terms Term.declare_free_names); fun thm_of_atom thm Ts = let diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Sat Nov 30 23:30:36 2024 +0100 @@ -211,8 +211,8 @@ let fun rew_term Ts t = let - val frees = - map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts); + val names = Name.build_context (Term.declare_free_names t); + val frees = map Free (Name.invent_names names "xa" Ts); val t' = r (subst_bounds (frees, t)); fun strip [] t = t | strip (_ :: xs) (Abs (_, _, t)) = strip xs t; diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Syntax/syntax_ext.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/Syntax/syntax_trans.ML Sat Nov 30 23:30:36 2024 +0100 @@ -302,18 +302,18 @@ fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T); fun bound_vars vars body = - subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body); + subst_bounds (map mark_bound_abs (rev (Term.variant_frees body vars)), body); fun strip_abss vars_of body_of tm = let val vars = vars_of tm; val body = body_of tm; - val rev_new_vars = Term.rename_wrt_term body vars; + val new_vars = Term.variant_frees body vars; fun subst (x, T) b = if Name.is_internal x andalso not (Term.is_dependent b) then (Const ("_idtdummy", T), incr_boundvars ~1 b) else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b)); - val (rev_vars', body') = fold_map subst rev_new_vars body; + val (rev_vars', body') = fold_map subst (rev new_vars) body; in (rev rev_vars', body') end; @@ -322,7 +322,7 @@ (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); fun atomic_abs_tr' (x, T, t) = - let val [xT] = Term.rename_wrt_term t [(x, T)] + let val xT = singleton (Term.variant_frees t) (x, T) in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end; fun abs_ast_tr' asts = @@ -389,7 +389,7 @@ (* dependent / nondependent quantifiers *) fun print_abs (x, T, b) = - let val (x', _) = Name.variant x (Term.declare_term_names b Name.context) + let val x' = #1 (Name.variant x (Name.build_context (Term.declare_term_names b))) in (x', subst_bound (mark_bound_abs (x', T), b)) end; fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/axclass.ML Sat Nov 30 23:30:36 2024 +0100 @@ -280,12 +280,12 @@ 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 = map TFree (Name.invent_types_global Ss); val missing_params = Sign.complete_sort thy [c] |> maps (these o Option.map #params o try (get_info thy)) |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t)) - |> (map o apsnd o map_atyps) (K (Type (t, map TFree args))); + |> (map o apsnd o map_atyps) (K (Type (t, args))); in thy |> Global_Theory.store_thm (binding, th) diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/conjunction.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Pure/consts.ML --- a/src/Pure/consts.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/consts.ML Sat Nov 30 23:30:36 2024 +0100 @@ -313,7 +313,7 @@ fun rev_abbrev lhs rhs = let val (xs, body) = strip_abss (Envir.beta_eta_contract rhs); - val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []; + val vars = map (fn (x, T) => Var ((x, 0), T)) (Term.variant_frees body xs); in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end; in diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/logic.ML Sat Nov 30 23:30:36 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, map TFree (Name.invent_types_global 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; @@ -667,7 +667,7 @@ (*reverses parameters for substitution*) fun goal_params st i = let val gi = get_goal st i - val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi)) + val rfrees = map Free (rev (Term.variant_frees gi (strip_params gi))) in (gi, rfrees) end; fun concl_of_goal st i = diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/more_thm.ML Sat Nov 30 23:30:36 2024 +0100 @@ -349,12 +349,11 @@ val used_frees = Name.build_context o - Thm.fold_terms {hyps = true} Term.declare_term_frees; + Thm.fold_terms {hyps = true} Term.declare_free_names; fun used_vars i = Name.build_context o - (Thm.fold_terms {hyps = false} o Term.fold_aterms) - (fn Var ((x, j), _) => i = j ? Name.declare x | _ => I); + Thm.fold_terms {hyps = false} (Term.declare_var_names (fn j => i = j)); fun dest_all ct used = (case Thm.term_of ct of diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/name.ML --- a/src/Pure/name.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/name.ML Sat Nov 30 23:30:36 2024 +0100 @@ -29,10 +29,18 @@ val declare_renamed: string * string -> context -> context val is_declared: context -> string -> bool val invent: context -> string -> int -> string list + val invent': string -> int -> context -> string list * context + 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: context -> '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 + val variant_names: context -> (string * 'a) list -> (string * 'a) list + val variant_names_build: (context -> context) -> (string * 'a) list -> (string * 'a) list val variant_list: string list -> string list -> string list val enforce_case: bool -> string -> string val desymbolize: bool option -> string -> string @@ -126,7 +134,18 @@ in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end; in invs o clean end; +fun invent' x n ctxt = + let val xs = invent ctxt x n + in (xs, fold declare xs ctxt) 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 ctxt xs = invent_names ctxt aT xs; +fun invent_types_global xs = invent_types context xs; val invent_list = invent o make_context; @@ -155,6 +174,9 @@ fun variant_bound name = variant (if is_bound name then "u" else name); +fun variant_names ctxt xs = #1 (fold_map (variant o fst) xs ctxt) ~~ map snd xs; +fun variant_names_build f xs = variant_names (build_context f) xs; + fun variant_list used names = #1 (make_context used |> fold_map variant names); diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/primitive_defs.ML Sat Nov 30 23:30:36 2024 +0100 @@ -77,8 +77,8 @@ fun abs_def eq = let val body = Term.strip_all_body eq; - val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); - val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); + val vars = map Free (Term.variant_frees body (Term.strip_all_vars eq)); + val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (rev vars, body)); val (lhs', args) = Term.strip_comb lhs; val rhs' = fold_rev (absfree o dest_Free) args rhs; in (lhs', rhs') end; diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/term.ML --- a/src/Pure/term.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/term.ML Sat Nov 30 23:30:36 2024 +0100 @@ -151,10 +151,14 @@ val add_frees: term -> (string * typ) list -> (string * typ) list val add_const_names: term -> string list -> string list val add_consts: term -> (string * typ) list -> (string * typ) list + val declare_tfree_namesT: typ -> Name.context -> Name.context + val declare_tfree_names: term -> Name.context -> Name.context + val declare_tvar_namesT: (int -> bool) -> typ -> Name.context -> Name.context + val declare_tvar_names: (int -> bool) -> term -> Name.context -> Name.context + val declare_free_names: term -> Name.context -> Name.context + val declare_var_names: (int -> bool) -> term -> Name.context -> Name.context val hidden_polymorphism: term -> (indexname * sort) list - val declare_typ_names: typ -> Name.context -> Name.context val declare_term_names: term -> Name.context -> Name.context - val declare_term_frees: term -> Name.context -> Name.context val variant_frees: term -> (string * 'a) list -> (string * 'a) list val smash_sortsT_same: sort -> typ Same.operation val smash_sortsT: sort -> typ -> typ @@ -162,7 +166,6 @@ val strip_sortsT_same: typ Same.operation val strip_sortsT: typ -> typ val strip_sorts: term -> term - val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list val eq_ix: indexname * indexname -> bool val eq_tvar: (indexname * sort) * (indexname * sort) -> bool val eq_var: (indexname * typ) * (indexname * typ) -> bool @@ -573,6 +576,12 @@ val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I); val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I); val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I); +val declare_tfree_namesT = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); +val declare_tfree_names = fold_types declare_tfree_namesT; +fun declare_tvar_namesT pred = fold_atyps (fn TVar ((a, i), _) => pred i ? Name.declare a | _ => I); +val declare_tvar_names = fold_types o declare_tvar_namesT; +val declare_free_names = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); +fun declare_var_names pred = fold_aterms (fn Var ((x, i), _) => pred i ? Name.declare x | _ => I); (*extra type variables in a term, not covered by its type*) fun hidden_polymorphism t = @@ -586,22 +595,15 @@ (* renaming variables *) -val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); - fun declare_term_names tm = fold_aterms (fn Const (a, _) => Name.declare (Long_Name.base_name a) | Free (a, _) => Name.declare a | _ => I) tm #> - fold_types declare_typ_names tm; - -val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); + declare_tfree_names tm; fun variant_frees t frees = - fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~ - map snd frees; - -fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) + Name.variant_names_build (declare_term_names t) frees; (* sorts *) @@ -812,7 +814,7 @@ of bound variables and implicit eta-expansion*) fun strip_abs_eta k t = let - val used = fold_aterms declare_term_frees t Name.context; + val used = Name.build_context (fold_aterms declare_free_names t); fun strip_abs t (0, used) = (([], t), (0, used)) | strip_abs (Abs (v, T, t)) (k, used) = let @@ -1074,7 +1076,7 @@ Abs (x, T, b) => if used_free x b then let - val used = Name.build_context (declare_term_frees b); + val used = Name.build_context (declare_free_names b); val x' = #1 (Name.variant x used); in subst_abs (x', T) b end else subst_abs (x, T) b diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/theory.ML --- a/src/Pure/theory.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/theory.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/thm.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Pure/type.ML --- a/src/Pure/type.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/type.ML Sat Nov 30 23:30:36 2024 +0100 @@ -345,9 +345,7 @@ val xs = build (t |> (Term.fold_types o Term.fold_atyps) (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I)); - val used = - Name.build_context (t |> - (fold_types o fold_atyps) (fn TVar ((a, _), _) => Name.declare a | _ => I)); + val used = Name.build_context (t |> Term.declare_tvar_names (K true)); val ys = #1 (fold_map Name.variant (map #1 xs) used); in map2 (fn (a, S) => fn b => ((a, S), ((b, 0), S))) xs ys end; diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/type_infer.ML Sat Nov 30 23:30:36 2024 +0100 @@ -109,13 +109,11 @@ fun subst_param (xi, S) (inst, used) = if is_param xi then - let - val [a] = Name.invent used Name.aT 1; - val used' = Name.declare a used; + let val ([a], used') = Name.invent' Name.aT 1 used; in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end else (inst, used); val params = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set; - val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt); + val used = fold Term.declare_tfree_names ts (Variable.names_of ctxt); val (inst, _) = fold subst_param params (TVars.empty, used); in (Same.commit o Same.map o Term.map_types_same) (Term_Subst.instantiateT_same inst) ts end; diff -r ed766dfdd2f1 -r 878bc24681d9 src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Pure/variable.ML Sat Nov 30 23:30:36 2024 +0100 @@ -17,13 +17,13 @@ val def_sort: Proof.context -> indexname -> sort option val declare_maxidx: int -> Proof.context -> Proof.context val declare_names: term -> Proof.context -> Proof.context + val variant_names: Proof.context -> (string * 'a) list -> (string * 'a) list val declare_constraints: term -> Proof.context -> Proof.context val declare_internal: term -> Proof.context -> Proof.context val declare_term: term -> Proof.context -> Proof.context val declare_typ: typ -> Proof.context -> Proof.context val declare_prf: Proofterm.proof -> Proof.context -> Proof.context val declare_thm: thm -> Proof.context -> Proof.context - val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list val bind_term: indexname * term -> Proof.context -> Proof.context val unbind_term: indexname -> Proof.context -> Proof.context val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context @@ -211,17 +211,19 @@ val declare_maxidx = map_maxidx o Integer.max; -(* names *) +(* type/term names *) fun declare_type_names t = - map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> + map_names (Term.declare_tfree_names t) #> map_maxidx (fold_types Term.maxidx_typ t); fun declare_names t = declare_type_names t #> - map_names (fold_aterms Term.declare_term_frees t) #> + map_names (Term.declare_free_names t) #> map_maxidx (Term.maxidx_term t); +fun variant_names ctxt xs = Name.variant_names (names_of ctxt) xs; + (* type occurrences *) @@ -275,15 +277,6 @@ val declare_thm = Thm.fold_terms {hyps = true} declare_internal; -(* renaming term/type frees *) - -fun variant_frees ctxt ts frees = - let - val names = names_of (fold declare_names ts ctxt); - val xs = fst (fold_map Name.variant (map #1 frees) names); - in xs ~~ map snd frees end; - - (** term bindings **) @@ -444,6 +437,13 @@ fold new_fixed args #> pair (map (#2 o #1) args); +fun variant ctxt raw_xs = + let + val names = names_of ctxt; + val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs; + val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); + in (names', xs ~~ xs') end; + in fun add_fixes_binding bs ctxt = @@ -464,20 +464,13 @@ else (xs, fold Name.declare xs names); in ctxt |> new_fixes names' ((xs ~~ xs') ~~ map Binding.pos_of bs) end; -fun variant_names ctxt raw_xs = - let - val names = names_of ctxt; - val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs; - val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); - in (names', xs ~~ xs') end; - fun variant_fixes xs ctxt = - let val (names', vs) = variant_names ctxt xs; + let val (names', vs) = variant ctxt xs; in ctxt |> new_fixes names' (map (rpair Position.none) vs) end; fun bound_fixes xs ctxt = let - val (names', vs) = variant_names ctxt (map #1 xs); + val (names', vs) = variant ctxt (map #1 xs); val (ys, ctxt') = fold_map next_bound (map2 (fn (x', _) => fn (_, T) => (x', T)) vs xs) ctxt; val fixes = map2 (fn (x, _) => fn Free (y, _) => ((x, y), Position.none)) vs ys; in ctxt' |> new_fixes names' fixes end; @@ -594,7 +587,7 @@ fun invent_types Ss ctxt = let - val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; + val tfrees = Name.invent_types (names_of ctxt) Ss; val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; in (tfrees, ctxt') end; diff -r ed766dfdd2f1 -r 878bc24681d9 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Tools/Code/code_preproc.ML Sat Nov 30 23:30:36 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 ed766dfdd2f1 -r 878bc24681d9 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Tools/Code/code_thingol.ML Sat Nov 30 23:30:36 2024 +0100 @@ -255,9 +255,6 @@ fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false; -fun invent_params used tys = - Name.invent_names (Name.build_context used) "a" tys; - fun split_pat_abs ((NONE, ty) `|=> (t, _)) = SOME ((IVar NONE, ty), t) | split_pat_abs ((SOME v, ty) `|=> (t, _)) = SOME (case t of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } => @@ -276,7 +273,8 @@ in (v :: vs, t') end | unfold_abs_eta tys t = let - val vs = map (SOME o fst) (invent_params (declare_varnames t) tys); + val names = Name.build_context (declare_varnames t); + val vs = map SOME (Name.invent names "a" (length tys)); in (vs, t `$$ map IVar vs) end; fun satisfied_application wanted ({ dom, range, ... }, ts) = @@ -293,9 +291,8 @@ in (([], (ts1, rty)), ts2) end else let - val vs_tys = invent_params (fold declare_varnames ts) - (((take delta o drop given) dom)) - |> (map o apfst) SOME; + val names = Name.build_context (fold declare_varnames ts); + val vs_tys = (map o apfst) SOME (Name.invent_names names "a" (take delta (drop given dom))); in ((vs_tys, (ts @ map (IVar o fst) vs_tys, rty)), []) end end @@ -656,7 +653,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 ed766dfdd2f1 -r 878bc24681d9 src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Tools/IsaPlanner/isand.ML Sat Nov 30 23:30:36 2024 +0100 @@ -56,10 +56,7 @@ let val names = Variable.names_of ctxt - |> (fold o fold_aterms) - (fn Var ((a, _), _) => Name.declare a - | Free (a, _) => Name.declare a - | _ => I) ts; + |> fold (fn t => Term.declare_free_names t #> Term.declare_var_names (K true) t) ts; in fst (fold_map Name.variant xs names) end; (* fix parameters of a subgoal "i", as free variables, and create an diff -r ed766dfdd2f1 -r 878bc24681d9 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Tools/induct.ML Sat Nov 30 23:30:36 2024 +0100 @@ -607,7 +607,7 @@ let val maxidx = Thm.maxidx_of st; val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) - val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal)); + val params = Term.variant_frees goal (Logic.strip_params goal); in if not (null params) then (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ diff -r ed766dfdd2f1 -r 878bc24681d9 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Nov 29 10:35:47 2024 +0100 +++ b/src/Tools/nbe.ML Sat Nov 30 23:30:36 2024 +0100 @@ -339,11 +339,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.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)) + then Name.invent' v (k - 1) #>> (fn vs => (v, vs)) else pair (v, [])) vs names; val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames; fun subst_vars (t as IConst _) samepairs = (t, samepairs) @@ -381,8 +378,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 +432,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],