--- a/src/HOL/Inductive.thy Thu Nov 28 19:35:30 2024 +0100
+++ b/src/HOL/Inductive.thy Fri Nov 29 00:25:03 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 (fst (Name.variant "x" (Term.declare_free_names cs Name.context)));
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/Tools/Ctr_Sugar/case_translation.ML Thu Nov 28 19:35:30 2024 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Nov 29 00:25:03 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 (Term.declare_free_names t Name.context) 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 [] (Term.declare_free_names t Name.context) :: 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,7 +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_clause t [] (Term.declare_free_names t Name.context) ::
decode_cases u
| decode_cases _ = case_error "decode_cases";
@@ -562,7 +562,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 (Term.declare_free_names pat Name.context) rhs of
SOME (exp as Free _, clauses) =>
if Term.exists_subterm (curry (op aconv) exp) pat andalso
not (exists (fn (_, rhs') =>
--- a/src/Pure/Proof/proof_checker.ML Thu Nov 28 19:35:30 2024 +0100
+++ b/src/Pure/Proof/proof_checker.ML Fri Nov 29 00:25:03 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 Thu Nov 28 19:35:30 2024 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Nov 29 00:25:03 2024 +0100
@@ -212,7 +212,7 @@
fun rew_term Ts t =
let
val frees =
- map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
+ map Free (Name.invent (Term.declare_free_names t Name.context) "xa" (length Ts) ~~ Ts);
val t' = r (subst_bounds (frees, t));
fun strip [] t = t
| strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
--- a/src/Pure/more_thm.ML Thu Nov 28 19:35:30 2024 +0100
+++ b/src/Pure/more_thm.ML Fri Nov 29 00:25:03 2024 +0100
@@ -349,7 +349,7 @@
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
--- a/src/Pure/term.ML Thu Nov 28 19:35:30 2024 +0100
+++ b/src/Pure/term.ML Fri Nov 29 00:25:03 2024 +0100
@@ -151,10 +151,11 @@
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_free_names: 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
@@ -573,6 +574,9 @@
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;
+val declare_free_names = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
(*extra type variables in a term, not covered by its type*)
fun hidden_polymorphism t =
@@ -586,16 +590,12 @@
(* 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)) ~~
@@ -812,7 +812,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 = fold_aterms declare_free_names t Name.context;
fun strip_abs t (0, used) = (([], t), (0, used))
| strip_abs (Abs (v, T, t)) (k, used) =
let
@@ -1074,7 +1074,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/type_infer.ML Thu Nov 28 19:35:30 2024 +0100
+++ b/src/Pure/type_infer.ML Fri Nov 29 00:25:03 2024 +0100
@@ -115,7 +115,7 @@
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 Thu Nov 28 19:35:30 2024 +0100
+++ b/src/Pure/variable.ML Fri Nov 29 00:25:03 2024 +0100
@@ -214,12 +214,12 @@
(* names *)
fun declare_type_names t =
- map_names (fold_types 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 (Term.declare_term_frees t) #>
+ map_names (Term.declare_free_names t) #>
map_maxidx (Term.maxidx_term t);