--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Apr 18 14:19:41 2025 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue Apr 22 17:35:02 2025 +0100
@@ -202,8 +202,8 @@
   unfolding bounded_def
   apply clarify
   apply (rule_tac x="x $ i" in exI)
-  apply (rule_tac x="e" in exI)
-  apply clarify
+  apply (rule_tac x="\<epsilon>" in exI)
+  apply clarify  
   apply (rule order_trans [OF dist_vec_nth_le], simp)
   done