# HG changeset patch
# User wenzelm
# Date 1732875977 -3600
# Node ID f76a5849b570e8b9469c4360a3ec09a5be43d462
# Parent  01f2936ec85e00d5a112cf42a5ff6424bf53e30e
tuned: more standard Name.build_context, although that is a bit longer;

diff -r 01f2936ec85e -r f76a5849b570 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Nov 29 00:25:03 2024 +0100
+++ b/src/HOL/Inductive.thy	Fri Nov 29 11:26:17 2024 +0100
@@ -532,7 +532,7 @@
   let
     fun fun_tr ctxt [cs] =
       let
-        val x = Syntax.free (fst (Name.variant "x" (Term.declare_free_names 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
diff -r 01f2936ec85e -r f76a5849b570 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Nov 29 00:25:03 2024 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Nov 29 11:26:17 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_free_names 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_free_names 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 $
@@ -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_free_names 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 =
@@ -562,7 +561,7 @@
   | encode_case _ _ = case_error "encode_case";
 
 fun strip_case' ctxt d (pat, rhs) =
-  (case dest_case ctxt d (Term.declare_free_names 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 01f2936ec85e -r f76a5849b570 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Nov 29 00:25:03 2024 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Nov 29 11:26:17 2024 +0100
@@ -212,7 +212,8 @@
     fun rew_term Ts t =
       let
         val frees =
-          map Free (Name.invent (Term.declare_free_names t Name.context) "xa" (length Ts) ~~ Ts);
+          map Free
+            (Name.invent (Name.build_context (Term.declare_free_names t)) "xa" (length Ts) ~~ Ts);
         val t' = r (subst_bounds (frees, t));
         fun strip [] t = t
           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
diff -r 01f2936ec85e -r f76a5849b570 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Fri Nov 29 00:25:03 2024 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Fri Nov 29 11:26:17 2024 +0100
@@ -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 01f2936ec85e -r f76a5849b570 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Nov 29 00:25:03 2024 +0100
+++ b/src/Pure/term.ML	Fri Nov 29 11:26:17 2024 +0100
@@ -598,8 +598,8 @@
   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;
+  #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!*)
 
@@ -812,7 +812,7 @@
   of bound variables and implicit eta-expansion*)
 fun strip_abs_eta k t =
   let
-    val used = fold_aterms declare_free_names 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