diff -r ea79448eb426 -r 678c3648067c src/HOL/Multivariate_Analysis/Weierstrass.thy
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Dec 22 14:31:39 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Dec 22 15:21:31 2015 +0100
@@ -203,7 +203,7 @@
     apply (rule cSUP_upper, assumption)
     by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)
 
-lemma normf_least: "s \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> s \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
+  lemma normf_least: "s \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> s \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
     by (simp add: normf_def cSUP_least)
 
 end