diff -r 6108dddad9f0 -r f0e07600de47 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 17 13:59:10 2017 +0100
@@ -2572,7 +2572,7 @@
         moreover have False if "1 < dd (x - a)"
           using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
           by (auto simp: rel_frontier_def)
-        ultimately have "dd (x - a) = 1" --\<open>similar to another proof above\<close>
+        ultimately have "dd (x - a) = 1" \<comment>\<open>similar to another proof above\<close>
           by fastforce
         with that show ?thesis
           by (simp add: rel_frontier_def)