diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -372,7 +372,7 @@
   shows "uniformly_convergent_on (ball z d) (\<lambda>n z. ln_Gamma_series z n :: complex)"
 proof (intro Cauchy_uniformly_convergent uniformly_Cauchy_onI')
   fix e :: real assume e: "e > 0"
-  define e'' where "e'' = (SUP t:ball z d. norm t + norm t^2)"
+  define e'' where "e'' = (SUP t\<in>ball z d. norm t + norm t^2)"
   define e' where "e' = e / (2*e'')"
   have "bounded ((\<lambda>t. norm t + norm t^2) ` cball z d)"
     by (intro compact_imp_bounded compact_continuous_image) (auto intro!: continuous_intros)
@@ -2270,7 +2270,7 @@
     qed
     ultimately have compact: "compact B" by (subst compact_eq_bounded_closed) blast
 
-    define M where "M = (SUP z:B. norm (h' z))"
+    define M where "M = (SUP z\<in>B. norm (h' z))"
     have "compact (h' ` B)"
       by (intro compact_continuous_image continuous_on_subset[OF h'_cont] compact) blast+
     hence bdd: "bdd_above ((\<lambda>z. norm (h' z)) ` B)"