tuned op's

--- a/src/HOL/Analysis/Path_Connected.thy	Thu Dec 21 19:55:41 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Dec 21 20:15:04 2017 +0100
@@ -2282,7 +2282,7 @@
   assumes 2: "2 \<le> DIM('N)" and pc: "path_connected {r. 0 \<le> r \<and> P r}"
   shows "path_connected {x. P(norm(x - a))}"
 proof -
-  have "{x. P(norm(x - a))} = op+a ` {x. P(norm x)}"
+  have "{x. P(norm(x - a))} = op+ a ` {x. P(norm x)}"
     by force
   moreover have "path_connected {x::'N. P(norm x)}"
   proof -