diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -202,7 +202,7 @@
     by (induct I rule: finite_induct; simp add: const mult)
 
   definition%important normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
-    where "normf f \<equiv> SUP x:S. \<bar>f x\<bar>"
+    where "normf f \<equiv> SUP x\<in>S. \<bar>f x\<bar>"
 
   lemma%unimportant normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
     apply (simp add: normf_def)