src/HOL/Tools/Ctr_Sugar/case_translation.ML

--- 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') =>