src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Nov 18 10:12:37 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Nov 18 15:23:34 2015 +0000
@@ -6882,7 +6882,6 @@
   fixes s :: "real set"
   assumes "continuous_on {t \<in> s. t \<le> a} f"
       and "continuous_on {t \<in> s. a \<le> t} g"
-      and "continuous_on s h"
       and "a \<in> s \<Longrightarrow> f a = g a"
     shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))"
 using assms