src/HOL/Multivariate_Analysis/Path_Connected.thy

--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -976,8 +976,7 @@
     apply (auto split: split_if_asm)
     done
   have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
-    unfolding field_divide_inverse
-    by (simp add: continuous_intros)
+    by (auto intro!: continuous_intros)
   then show ?thesis
     unfolding * **
     using path_connected_punctured_universe[OF assms]