--- a/src/HOL/Limits.thy Sun Nov 22 23:19:43 2015 +0100
+++ b/src/HOL/Limits.thy Mon Nov 23 16:57:54 2015 +0000
@@ -631,7 +631,7 @@
unfolding continuous_def by (rule tendsto_diff)
lemma continuous_on_diff [continuous_intros]:
- fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
unfolding continuous_on_def by (auto intro: tendsto_diff)