Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Ctr_Sugar/case_translation.ML
changeset 81543 fa37ee54644c
parent 81521 1bfad73ab115 
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Dec 06 13:33:25 2024 +0100
@@ -477,7 +477,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 (Name.variant_names (Term.declare_term_names u used) xs);
+            val xs' = map Free (Name.variant_names (Term.declare_free_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 =
isabelle