# HG changeset patch
# User wenzelm
# Date 1733084037 -3600
# Node ID 13e9678f2c00e67be8457de9ee053aa839b1a7cf
# Parent  06eebdc93ea8b3fea864f1fa6b408992ce28c5f7
clarified names context: proper context, without consts;

diff -r 06eebdc93ea8 -r 13e9678f2c00 src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Sun Dec 01 18:12:24 2024 +0100
+++ b/src/HOL/Analysis/metric_arith.ML	Sun Dec 01 21:13:57 2024 +0100
@@ -102,8 +102,10 @@
     (case find ct of
       [] =>
         (*if no point can be found, invent one*)
-        let val x = singleton (Term.variant_frees (Thm.term_of ct)) ("x", metric_ty)
-        in [Thm.cterm_of ctxt (Free x)] end
+        let
+          val names = Variable.names_of ctxt |> Term.declare_free_names (Thm.term_of ct)
+          val x = Free (#1 (Name.variant "x" names), metric_ty)
+        in [Thm.cterm_of ctxt x] end
     | points => points)
   end