diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Limits.thy
--- 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)