--- 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
--- 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>\<open>no\<close> 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:
--- 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)
--- 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),
--- 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);
--- 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>\<open>_lam_pats_syntax\<close>, fun_tr)] end
--- 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;
--- 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 =
--- 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)
--- 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
--- 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". *)
--- 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
--- 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);
--- 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 []
--- 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)))
--- 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>\<open>type\<close>)) (Name.invent Name.context Name.aT n);
+ val As = map (fn a => TFree (a, \<^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/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>\<open>_case1\<close>, _) $ 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>\<open>case_elem\<close> $ Term_Position.strip_positions l' $ r)
end
@@ -198,7 +198,7 @@
fun mk_clauses (Const (\<^const_syntax>\<open>case_nil\<close>, _)) = []
| mk_clauses (Const (\<^const_syntax>\<open>case_cons\<close>, _) $ 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>\<open>_case_syntax\<close> $ 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>\<open>undefined\<close>, 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>\<open>case_nil\<close>, _)) = []
| decode_cases (Const (\<^const_name>\<open>case_cons\<close>, _) $ 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') =>
--- 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>\<open>undefined\<close>, rT))
--- 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
--- 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, ...}) =
--- 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>\<open>bool\<close>), ("x", HOLogic.mk_tupleT Ts)]
+ Variable.variant_names ctxt [("P", \<^typ>\<open>bool\<close>), ("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));
--- 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
--- 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
--- 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
--- 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))
--- 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"
--- 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'
--- 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
--- 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>\<open>narrowing_term\<close>) tys))
+ val frees = map (fn a => Free (a, \<^typ>\<open>narrowing_term\<close>)) (Name.invent_global "a" (length 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/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
--- 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>\<open>Random.seed\<close>
(HOLogic.mk_valtermify_app c vs simpleT);
val t = HOLogic.mk_ST
--- 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 $
--- 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 *)
--- 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,
--- 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);
--- 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>\<open>gfp predT\<close> else \<^Const>\<open>lfp predT\<close>;
+ 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)
--- 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>\<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 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>\<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/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);
--- 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 " ^
--- 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;
--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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
--- 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;
--- 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 =
--- 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) =
--- 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)
--- 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";
--- 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
--- 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 =
--- 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
--- 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);
--- 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;
--- 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
--- 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 =
--- 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
--- 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;
--- 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;
--- 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;
--- 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 =
--- 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';
--- 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
--- 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): " ^
--- 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],