# HG changeset patch
# User wenzelm
# Date 1732990898 -3600
# Node ID 31b05aef022d3dc2e9d3153d235764ff66d9fd57
# Parent  44c0028486db0f003d5bc871ef79b61696e312e3
eliminate historic clone (see also 550e36c6a2d1);

diff -r 44c0028486db -r 31b05aef022d src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Library/refute.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/Provers/preorder.ML
--- a/src/Provers/preorder.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Provers/preorder.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Sat Nov 30 19:21:38 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 =
diff -r 44c0028486db -r 31b05aef022d src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/consts.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/logic.ML	Sat Nov 30 19:21:38 2024 +0100
@@ -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 44c0028486db -r 31b05aef022d src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/primitive_defs.ML	Sat Nov 30 19:21:38 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 44c0028486db -r 31b05aef022d src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/term.ML	Sat Nov 30 19:21:38 2024 +0100
@@ -166,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
@@ -607,8 +606,6 @@
   #1 (fold_map Name.variant (map fst frees) (Name.build_context (declare_term_names t))) ~~
     map #2 frees;
 
-fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
-
 
 (* sorts *)
 
diff -r 44c0028486db -r 31b05aef022d src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Tools/induct.ML	Sat Nov 30 19:21:38 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): " ^